Sarek Høverstad Skotåm
Sarek Høverstad Skotåm
Upcasting an integer causes a "violent" panic. For instance: ```rust fn test(inp: u8) { let bing = inp as usize; } ``` results in the following backtrace: ``` thread 'rustc'...
Casting a `bool` to any integer type, as in for instance: ```rust let bing = false as u8; ``` currently yields `error[creusot]: Non integral casts are currently unsupported`
Making a function `const` and running Creusot causes the following stack trace: ``` thread 'rustc' panicked at 'attempted to read from stolen value: rustc_middle::mir::Body', creusot/src/translation/function.rs:61:25 stack backtrace: 0: 0x7f764d49e94d -...
```rust #[predicate] pub fn ex() -> bool { true } #[predicate] pub fn ex_() -> bool { true } #[logic] fn lemma() { ex(); } ``` causes the error `File...
Not super important, but might as well report(especially since it seems to be solvable in the parser). The following ```rust extern crate creusot_contracts; use creusot_contracts::*; use creusot_contracts::std::*; #[predicate] pub fn...
Not super important, but if one forgets to add `#[logic]`/`#[predicate]` and uses the `pearlite!` macro, Creusot will not complain. I think it would be better if it is checked by...
``` rust #[predicate] #[ensures(1 === 1)] fn ok() -> bool { pearlite!{ true } } #[logic] #[requires(1 === 1)] fn errs() -> bool{ pearlite!{ exists true } } #[predicate] #[ensures(1...
Deriving `Eq` works just fine, whereas deriving `PartialEq` gives the following error: ``` thread 'rustc' panicked at 'not implemented', creusot/src/translation/traits.rs:246:14 ``` Example: ``` #[derive(PartialEq)] enum Example { Example, Example2 }...
When figuring out the proof, it is sometimes useful to add `#[trusted]` temporarily. If that function has a `#[variant]` attached, Why3 will give the following error: `unexpected 'variant' clause` Example:...
Early returns in while-loops, as in: ``` fn example() -> bool { let mut j = 0; let loop_len = 5; #[invariant(loop_bound2, 0usize