No panic detected on unwrap with None type

[zpzigi754]

With the below code containing a panic, prusti gave out Successful verification of 2 items.

fn test() {
      let a: usize = None.unwrap();
}

fn main() {}

As check_panics option is in default set, I expected the message like statement might panic. Does this mean that prusti's panic check could have a false negative result?

[Aurel300]

Thanks for the report! This is because Prusti does not know anything about Option::unwrap (and it is just a method like any other), so it has no reason to report a panic. For now, you need to provide an extern spec for Option to attach contracts to some of the methods, see this example.

In the long-term we want to make this more practical of course: we will provide specifications for the standard library with the tool or an additional crate.

[zpzigi754]

For now, you need to provide an extern spec for Option to attach contracts to some of the methods, see this example.

Thanks for the quick resonse! I've confirmed that the panic is caught when I've provided the extern spec as guided. Does this mean that I should explicitly define the above extern spec for std::option::Option in every crate I use the Option? I've defined the extern_spec in one separate crate and tried to import it from another crate, but extern_spec do not seem to work.

For example,

// crate option
#![no_std]
extern crate prusti_contracts;
use prusti_contracts::*;

#[extern_spec]
impl<T> core::option::Option<T> {
    #[pure]
    #[ensures(matches!(*self, Some(_)) == result)]
    pub fn is_some(&self) -> bool;

    #[pure]
    #[ensures(self.is_some() == !result)]
    pub fn is_none(&self) -> bool;

    #[requires(self.is_some())]
    pub fn unwrap(self) -> T;
...

// crate test (the above crate is imported in Cargo.toml)
#![no_std]
use option;

fn test() {
      let a: usize = None.unwrap();
}

In the above setting where extern_spec is defined in another crate and imported, cargo-prusti does not seem to use the extern_spec: it has failed to report an error.

[Aurel300]

Exporting specifications across crate boundaries is also something we are actively working on.

[fpoli]

Related issues: https://github.com/viperproject/prusti-dev/issues/2 and https://github.com/viperproject/prusti-dev/issues/910