prusti-dev icon indicating copy to clipboard operation
prusti-dev copied to clipboard

Unexpected internal error using HashMap.get()

Open pinzaghi opened this issue 3 years ago • 1 comments

I'm having the following error

error: [Prusti internal error] Prusti encountered an unexpected internal error
 --> /src/test.rs:8:13
  |
8 |     let a = h.get(i).unwrap()-1;
  |             ^^^^^^^^
  |

with this code:

#![feature(box_patterns)]
use prusti_contracts::*;
use std::collections::HashMap;

#[ensures(true)]
fn test(h: HashMap<u64, u64>, i: &u64) {
    let a = h.get(i).unwrap();
}
fn main(){}

and this version (I also tried the latest nightly build):

Prusti version: commit 164fa35 2022-03-15 20:32:24 UTC, built on 2022-03-15 21:59:32 UTC rustc 1.61.0-nightly (285fa7ecd 2022-03-14)

pinzaghi avatar Apr 08 '22 13:04 pinzaghi

Reference-typed fields are not yet supported (get returns Option<&u64>).

vakaras avatar Apr 09 '22 19:04 vakaras