Open
Description
Minimal example:
pub fn main() {
let a = 3;
let b = Some(&a);
}The error:
error: [Prusti internal error] Prusti encountered an unexpected internal error
--> e25-wrapping-borrow.rs:1:1
|
1 | / pub fn main() {
2 | | let a = 3;
3 | | let b = Some(&a);
4 | | }
| |_^
|
= note: We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new
= note: Details: cannot generate fold-unfold Viper statements. The required permission Acc(_3.val_ref.val_int, read) cannot be obtained.
In fact, any form of instantiating a struct with a reference field seems to fail. Another example which gives an error:
struct RefInt<'a>(&'a i32);
pub fn main() {
let a = 3;
let b = RefInt(&a);
}