Patricio Inzaghi

Help with HashMap / get_and_unwrap specification

8

I am trying to use the function [get_and_unwrap](https://github.com/viperproject/prusti-dev/issues/1029) which has the precondition `requires(map.contains_key(key))`. My HashMap spec looks like this: ``` #[extern_spec] impl HashMap where K: Eq + Hash, S: BuildHasher,...

Unexpected internal error using HashMap.get()

1

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...

List tutorial fails to verify

6

I am trying to verify (using the prusti-rustc binary) the basic stack proposed in the tutorial: ``` #![feature(box_patterns)] use prusti_contracts::*; use std::mem; pub enum TrustedOption { Some(i32), None, } pub...

hashmaps3 double borrow

1

Hello, I am new with Rust! Trying to solve the exercise like this: ``` let team1 = Team {goals_scored: 0, goals_conceded: 0}; let entry1 = scores.entry(team_1_name).or_insert(team1); let team2 = Team...