Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Passing two references as arguments triggers panic #29

Closed
frececroka opened this issue May 6, 2020 · 2 comments
Closed

Passing two references as arguments triggers panic #29

frececroka opened this issue May 6, 2020 · 2 comments
Labels
error-reporting Something needs to be fixed in the error reporting

Comments

@frececroka
Copy link
Contributor

frececroka commented May 6, 2020 •
edited by fpoli
Loading

This causes Prusti to panic:

use prusti_contracts::*;

struct Point { x: u32, y: u32 }

fn foo<'a, 'b>(p: &'a mut Point, q: &'b mut Point) -> &'a mut u32 {
    &mut p.x
}

fn main(){}
@fpoli
Copy link
Member

fpoli commented May 7, 2020 •
edited
Loading

Calling functions with multiple lifetimes is currently unsupported.

@fpoli fpoli added bug Something isn't working error-reporting Something needs to be fixed in the error reporting and removed bug Something isn't working labels May 7, 2020
f4z3r pushed a commit to f4z3r/prusti-dev that referenced this issue Jun 2, 2020
started work on two pass parser with register, viperproject#29
43b6391
f4z3r pushed a commit to f4z3r/prusti-dev that referenced this issue Jun 2, 2020
started work on two pass parser with register, viperproject#29
5cab1bf
f4z3r pushed a commit to f4z3r/prusti-dev that referenced this issue Jun 3, 2020
improved register, viperproject#29
f7c1920
@fpoli
Copy link
Member

fpoli commented Dec 2, 2020

The example now seems to work fine.

@fpoli fpoli closed this as completed Dec 2, 2020
@fpoli fpoli reopened this Dec 2, 2020
@fpoli fpoli closed this as completed Dec 2, 2020
JonasAlaif added a commit to zgrannan/prusti-dev that referenced this issue Nov 29, 2023
@JonasAlaif @Aurel300
Cleanup, derive task encoder caches (viperproject#29)
784c15e 
* remove unused feature attrs

* macro to derive task encoder cache

* remove stale code comments

---------

Co-authored-by: Aurel Bílý <aurel.bily@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
error-reporting Something needs to be fixed in the error reporting
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@frececroka @fpoli