viperproject / prusti-dev

A static verifier for Rust, based on the Viper verification infrastructure.
http://prusti.org
Other
1.55k stars 106 forks source link

Prusti encounters unexpected internal error on return types containing references #1457

Open benjaminflin opened 1 year ago

benjaminflin commented 1 year ago

Minimal reproduction:

fn foo(input: &u8) -> Option<&u8> {
    Some(input)
}
error: [Prusti: internal error] Prusti encountered an unexpected internal error
  --> sediment/src/parsing/mod.rs:10:1
   |
10 | / fn foo(input: &u8) -> Option<&u8> {
11 | |     Some(input)
12 | | }
   | |_^
   |
   = note: This is likely to be a bug in Prusti. We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new
   = note: Details: cannot generate fold-unfold Viper statements. Failed to subtract fractional permissions: invalid substraction: read - write.
vakaras commented 1 year ago

References inside structs are not yet supported.