creusot

creusot copied to clipboard

Closures are normally used with short, straight-line bodies and are meant to be lightweight. Having to specify a contract for closures is tedious and removes a lot of the ergonomic reasons to use them. Luckily, Why3, does support treating function bodies as whiteboxes, so we should be able to use the WP of a closure as its contract.

Hi!

Currently the error message for a closure without an explicit contract is not very clear.

A file containing only:

pub fn foo() {
    let f = || {};
}

gives me

warning: unused variable: `f`
 --> proto/src/lib.rs:2:9
  |
2 |     let f = || {};
  |         ^ help: if this is intentional, prefix it with an underscore: `_f`
  |
  = note: `#[warn(unused_variables)]` on by default

warning: the `creusot_contracts` crate is not loaded. You will not be able to verify any code using Creusot until you do so.
  |
  = note: `#[warn(creusot::resolve_trait)]` on by default

thread 'rustc' panicked at 'called `Option::unwrap()` on a `None` value', creusot/src/translation/function.rs:493:87
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

note: Creusot has panic-ed!
  |
  = note: Oops, that shouldn't have happened, sorry about that.
  = note: Please report this bug over here: https://github.com/xldenis/creusot/issues/new

warning: `proto` (lib) generated 2 warnings (run `cargo fix --lib -p proto` to apply 1 suggestion)
error: could not compile `proto` (lib); 2 warnings emitted

Depending on the ETA to handle closures without explicit contracts, it may be useful to first try to have a clearer error message.

Cheers,

I think from the other output the issue is actually that you didn't add creusot_contracts you your dependencies. Though I agree the error should be better (and I thought it was..)

Interestingly, it was in my Cargo.toml but I hadn't added the use creusot_contracts.

FWIW:

// this alone works
pub fn foo() {
}

// this works as well
use creusot_contracts;
pub fn foo() {
    let f = || {};
}

// this does not
pub fn foo() {
    let f = || {};
}

Yea, unfortunately if you never actually use a crate it's not "really" loaded, just available. I'll fix the error so it doesn't ICE though.