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.

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

Unimplemented: Inhale the predicate rooted at dst_field #49

Closed
karlosss opened this issue Jun 8, 2020 · 4 comments · Fixed by #1126
Closed

Unimplemented: Inhale the predicate rooted at dst_field #49

karlosss opened this issue Jun 8, 2020 · 4 comments · Fixed by #1126
Labels
bug Something isn't working

Comments

@karlosss
Copy link
Contributor

karlosss commented Jun 8, 2020

This program

use prusti_contracts::*;
use std::collections::HashSet;
use std::hash::Hash;
use std::cmp::Eq;

struct SetWrapper<T: Hash + Eq> {
    set: HashSet<T>
}

impl<T: Hash + Eq> SetWrapper<T> {
    #[pure]
    #[trusted]
    pub fn contains(&self, value: &T) -> bool {
        self.set.contains(value)
    }

    #[ensures(self.contains(&value))]
    pub fn insert(&mut self, value: T) {
        self.set.insert(value);
    }

    #[ensures(!self.contains(&value))]
    pub fn remove(&mut self, value: &T) -> bool {
        self.set.remove(value)
    }
}

fn test() {
    let mut set = SetWrapper { set: HashSet::new() };
    set.insert(1);
    set.insert(2);
    set.insert(3);
    set.remove(&3);
    set.remove(&2);
    set.remove(&1);
    set.remove(&1);
}

fn main() {}

crashes with

thread 'main' panicked at 'not yet implemented: Inhale the predicate rooted at dst_field.', prusti-viper/src/encoder/procedure_encoder.rs:3973:25
@fpoli fpoli added the bug Something isn't working label Jun 8, 2020
@fpoli fpoli changed the title Inhale the predicate rooted at dst_field Unimplemented: Inhale the predicate rooted at dst_field Jun 17, 2020
@fpoli
Copy link
Member

fpoli commented Dec 2, 2020

Prusti no longer crashes, and the output is now the following:

error: [Prusti: unsupported feature] the encoding of this reference copy has not been implemented
  --> tmp/program.rs:34:16
   |
34 |     set.remove(&3);
   |                ^^

error: [Prusti internal error] generating fold-unfold Viper statements failed (FailedToObtain(Pred(Local(_2: Ref(__TYPARAM__$T$__), Position { line: 18, column: 15, id: 168 }), read)))
  --> tmp/program.rs:19:5
   |
19 | /     pub fn insert(&mut self, value: T) {
20 | |         self.set.insert(value);
21 | |     }
   | |_____^

error: [Prusti: verification error] postcondition might not hold.
  --> tmp/program.rs:23:15
   |
23 |     #[ensures(!self.contains(&value))]
   |               ^^^^^^^^^^^^^^^^^^^^^^
   |
note: the error originates here
  --> tmp/program.rs:24:5
   |
24 | /     pub fn remove(&mut self, value: &T) -> bool {
25 | |         self.set.remove(value)
26 | |     }
   | |_____^

The "Prusti internal error" is still a bug.

@fpoli
Copy link
Member

fpoli commented Apr 22, 2021

The contract of insert is problematic: we would like to express #[ensures(self.contains(&old(value)))], but since value is of a generic type then old(value) raises an internal error. This should be fixed by #187.

@fpoli
Copy link
Member

fpoli commented Mar 24, 2022

Related to #418

Aurel300 referenced this issue in Aurel300/prusti-dev Aug 9, 2022
@Aurel300
Copy link
Member

Aurel300 commented Aug 9, 2022

Things work here except for the constants like &3. The workaround is to put the constant into a variable, then reference that variable.

@bors bors bot closed this as completed in 7cf7787 Aug 9, 2022
zgrannan added a commit to zgrannan/prusti-dev that referenced this issue May 18, 2024
zgrannan added a commit to zgrannan/prusti-dev that referenced this issue Jun 7, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
None yet
Development

Successfully merging a pull request may close this issue.

4 participants