aeneas

aeneas copied to clipboard

Let charon manage `Self` clauses

5

Companion PR to https://github.com/AeneasVerif/charon/pull/514. This removes the need for managing the special `Self` clause in methods ourselves. One consequence is that in https://github.com/AeneasVerif/charon/pull/514 I had to add a pass that...

Nadrieril

Unexpected error

5

Reported by @ Cemoixerestre. The following program triggers an "Unexpected" failure: ```rust fn f(a: &mut i32, b: &mut i32, c: &mut i32, conds : &[bool]) { let mut y =...

sonmarcho

sonmarcho

When I compile the simple "Hello World" program: ```rust fn main() { println!("Hello World!") } ``` I obtain the following error message: ``` [Info ] Imported: counter_example_aeneas.llbc Uncaught exception: (Failure...

Cemoixerestre

e.g., the process and annotations needed to use `charon::opaque` attributes

R1kM

Improve error message about bottoms

1

I have the following simplified code ``` struct UU(u32); const z : UU = UU(0u32); fn f(_ : UU) {} fn g() { let x = z; f(x); f(x); }...

shaoweilin

Improve the extraction of code manipulating arrays/slices

2

When extracting Rust code of the following shape: ```rust a[i] = x + y; ``` We get: ```lean let (_, index_mut_back) ← Array.index_mut_usize a i let tmp ← x +...

sonmarcho

External types are opaque, but we need to know if some of their lifetimes are used in mutable borrows or not to properly generate the backward functions. Example : ```rust...

sonmarcho

Once https://github.com/AeneasVerif/charon/pull/210 is merged and once associated types are lifted to become parameters we should remove this option: https://github.com/AeneasVerif/aeneas/blob/267526a271d5fe04e29fc21a87fbe0f733af33e3/tests/src/traits.rs#L2

sonmarcho

In the Lean backend, the `progress` tactic performs a lot of work to automate proofs and handle the Aeneas monadic translation. However, the current tactic also assumes particular shapes for...

R1kM