creusot

creusot copied to clipboard

This is a summary of some known issues with the current macros: - [ ] Invariants on for loops have broken spans - [ ] The ghost macro can generate...

xldenis

Is this something we want to do locally? If so we should figure out a simple test harness for it as manually specifying the paths in `tests/ui.rs` leaves a bit...

xldenis

Ghost code v2

11

In #381 we gained support for an initial version of ghost code based on an adhoc language consisting of the intersection of Rust and Pearlite. This ghost code has borrow...

xldenis

Ensures and requires clause order is reversed when translated into Why3

2

jhjourdan

Properly hide visibility of private fields

8

Private fields should not appear in a type for functions that don't have permission to see them.

xldenis

Translate Union names properly (allows BTreeMap).

xldenis

xldenis

Actually attempting to use a tuple constructor will trigger an error in creusot.

xldenis

- Challenge 1 - Challenge 2 - initial version - Challenge 3 - start cleaning up

xldenis

Add AddLogic and friends that can be used in pearlite.

2

jhjourdan