Xavier Denis

Tracking issue for improving Pearlite - [ ] #403 - [x] #435 - [x] #380 - [x] #301 - [x] #266 - [x] #261 - [ ] #117 - [x]...

Closures shouldn't need explicit contracts

4

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

State of `DeepModel` and `ShallowModel`.

35

I wonder if we we should re-evaluate the existence of both `DeepModel` and `ShallowModel`. Can we feasibly combine the two? Would it be excessive to get rid of `ShallowModel` entirely?

Crash reported

2

@jhaye reports that the following code creates ill typed why3 code. ```rust use creusot_contracts::*; /// A sparse map representation over a totally ordered key type. /// /// Used in [crate::ExecutableReactions]...

This PR implements the required hacks to make nested closures work. The short idea is that we really treat closures like two separate modules (which they *are*). Depending on the...

Type invariants cause unsound contracts for unspecified functions

5

When an external function has no contract, creusot might still add preconditions for type invariants. This interferes with the elaboration which adds `requires { false }` to those functions, resulting...

Running `cargo creusot` twice on the same project fails

1

There's a problem introduced by @voidc's `MIR_BODIES` patch where running `cargo creusot` twice on the same program causes it to crash saying: `thread 'rustc' panicked at 'called `Option::unwrap()` on a...

laws with unsatisfied where clauses shouldn't be loaded

1

in the following program: ``` extern crate creusot_contracts; use creusot_contracts::*; trait A { #[logic] fn a(self) -> Option; #[law] #[ensures(self.a() != None)] fn a_b(self) where Self: B; } trait B...

@fpoli pointed out that the mutex test case in Creusot is wrong. To be sound and faithful to RHB we should use a `Mapping` to hold our invariant (which we...