Xavier Denis

The intrinsic `discriminant_value` is used inside the proc macro for `Hash`, and causes it to crash. I haven't thought about why it crashes or the proper way to fix it...

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

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

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

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

Translate Union names properly (allows BTreeMap).

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

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

Error when user forgets to use `pearlite!`

2

We should detect and provide a helpful error when the user forgets to use `pearlite! { .. }` in predicates or logical functions. see #378