Lucas Franceschino
Lucas Franceschino
We want a phase that eliminates explicit control flow (say a `return` or a `break`) by moving or duplicating code. We want to rewrite the control flow so that every...
Rust desugars `assert!(condition)` as something like `if !condition {panic!()}`, which is not very nice looking. We should detect and rewrite those as calls to a hax-lib function, say, `hax::assert(condition)`
`detect_forking` intent is to discover which feature is enabled by running a `cargo build`. It uses a very simple custom driver, which stops right after parsing. This makes hax fail...
PR #614 adds support for new ways of inlining backend code within Rust. In the ProVerif backend, certain kinds of items (e.g. Fn vs Type) are outputted in different parts...
This issue is about any expression that can yield an early return: `?`, `return`, `continue`, `break`. The engine has a module `side_effect_utils.ml` that deals with any expression with side effects:...
For now, it's not possible to select `impl` blocks or `const _` items: those have no explicit name in Rust.
Currently methods are mostly translated as fields in dependent structs. Hositing methods out of impl blocks will be useful for: - F* when dealing with mutually recursive definitions within an...