Sarek Høverstad Skotåm

Compilation error on implementing `Default`

3

I cannot seem to find a way to implement `Default`. Ie: ```rust struct MyStruct {} impl Default for MyStruct { fn default() -> Self { Self {} } } ```...

MLCFG error when using contract involving division on an integer when function also takes a float.

2

Pretty odd issue tbh. ie: ```rust #[requires(x@ < (u32::MAX@ / 1))] fn div_err(f: f64, x: u32) {} ``` and: ```rust #[requires(x@ < usize::MAX@ / 1)] fn div_err(f: f64, x: usize)...

Implementing `Invariant` is just under twice as slow as creating a function called `invariant` and manually adding `requires`/`ensures`

2

NOTE: (Okay, I just remembered `#[why3::attr = "inline:trivial"]` exists, which, when added to the `fn invariant` in `Invariant` causes the two implementations to take roughly the same amount of time)....

MLCFG error on derefing `Arc`/`Rc` in contracts

3

```rust #[requires((*a)@ == 0)] fn test_arc(a: Arc) {} ``` gives: `File "../pt.mlcfg", line 53, characters 77-89: unbound function or predicate symbol 'Deref0.deref'` Same error for `Rc`.

Creusot panic

2

Could probably be reduced further, but, this code: ```rust struct Heap { activity: Vec, heap: Vec, indices: Vec, num_vars: usize, } impl Heap { pub(crate) fn new(n: usize) -> Self...

`Invariant` (with certain invariants) makes certain patterns (ie `IndexMut`) impossible to implement

2

Here exemplified with a `Heap` which implements `IndexMut`. The source of the conflict is ```rust && forall 0 self.heap@[i]@ < [email protected]() ``` in the `invariant` (as we have no way...

Creusot panic on model where `ShallowModelTy` is a tuple with a `Seq`.

1

The following code ```rust use creusot_contracts::*; pub struct Formula { vec: Vec, b: bool, } impl ShallowModel for Formula { type ShallowModelTy = (Seq, bool); #[logic] #[open] fn shallow_model(self) ->...

MLCFG error when deconstructing a tuple which also is used in a {pre, post}condition

1

This is a regression, meaning that the following pattern previously worked in CreuSAT, but now gives an MLCFG error. The following code: ```rust use creusot_contracts::*; #[logic] #[open(self)] // Opacity doesn't...

Currently the following: ```rust #[open] #[logic] fn my_logic_function() {} #[open] #[logic] pub fn my_pub_logic_function() { my_logic_function() } ``` would return the following error: ``` Cannot make `"my_logic_function"` transparent in `"my_pub_logic_function"`...