maximebuyse
maximebuyse
Passing a function as a value in a higher order context produces bad names in extracted codes. ```rust fn f(higher_order: impl FnOnce(()) -> ()) {} fn main() { // Next...
```rust #[allow(dead_code)] fn test() { let mut s = String::from("ab"); let b = s.pop(); } ``` [Open this code snippet in the playground](https://hax-playground.cryspen.com/#fstar/e94de4c52f/gist=7b444e223048c75a2ddff8f2fea30ecd)
When I run `cargo test --test toolchain` I get the following error: ``` /home/maxime/cryspen/hax/target/debug/cargo-hax: error while loading shared libraries: librustc_driver-f4e5b0d07cf2a17f.so: cannot open shared object file: No such file or directory...
`dyn` was added to the engine in https://github.com/hacspec/hax/issues/296 but it still need to be treated properly in the f* backend. `dyn (A + B)` is translated as `dyn 2 (fun...
Closes #393. Loops are already translated as folds. This PR wraps their accumulators to add control flow information (in case of `break` `return` or `continue`). Some specific fold operators are...
With rust code containing deep expressions, hax fails with a stack overflow. For example: ``` fn main() -> i32 { 1 + 1 + 1 + 1 + 1 +...
Closes #464 , #804 We add a phase to rewrite array patterns and usize/isize/i128/u128 patterns. The phase rewrites them with `if let` guards. For integer types the idea is to...
When an opaque type contains something that is rejected by hax, we produce an error but we could very well keep it as we are supposed to ignore what is...
Some additions to fstar core were made in the `cryspen-sandwich` branch. It would be great to upstream them to the `main` branch. However some more changes were made in this...