creusot

creusot copied to clipboard

Make verified conditions available to the optimizer

8

I would like to make the fact that certain conditions are verified to always hold available to the optimizer. With this, things like bounds checks or `unwrap`s that are verified...

LevitatingLion

Add support for upcasting of integer types

2

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

sarsko

Adds a specification for `[T]::iter_mut` and the associated `IterMut` type. One quirk is that where in RustHornBelt we modeled mutable iterators a sa sequence of borrows, I used a borrow...

xldenis

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`

sarsko

Bugs about ghost code.

4

Consider this piece of code: ```rust extern crate creusot_contracts; use creusot_contracts::*; struct S { g: Ghost } #[logic] fn prophecy(x: &mut S) -> i32 { pearlite!{ *(^x).g } } pub...

jhjourdan

Provide `cfg(creusot)`

3

It would be great if Creusot provided a `cfg(creusot)` when compiling under `cargo creusot`. This would remove the need for the `contracts` feature in `creusot-contracts`, since the Creusot-specific code could...

LevitatingLion

`creusot-contracts` should be tested in CI

2

We should actually generate the MLCFG and prove all the obligations in `creusot-contracts`. At the moment everything is `#[trusted]` but we should still check.

xldenis

Specifying a closure with multiple arguments causes why3 error

6

Example: ```rust use creusot_contracts::*; fn test() { let c = { #[requires(@x + @y < @u32::MAX)] #[ensures(@result == @x + @y)] |x: u32, y: u32| x + y }; let...

dewert99

Thanks to @jhjourdan's #376 we can actually replay complex sessions in CI, but this is still rather unfinished business. There are a few further improvements we could make which would...

xldenis

Program translation IR

1

I'm introducing an IR in the translation of program code which is non-why3 specific. It serves a few purposes: - Isolating the rest of Creusot from rustc's changes - Making...

xldenis