Expand description
The CLI options for cargo-hax. The types defines in this module
are also used by the driver and the engine.
Modules§
Structs§
- Backend
Options - Bounds
Options - Cargo
Hermeticity Options - Cargo’s hermeticity flags, applied to every cargo invocation a
cargo hax extractrun drives: project discovery, the frontend’scargo check, and the build charon drives. - Exporter
Options - The subset of
Optionsthe frontend is sensible to. - Extensible
Options - FStar
Options - Force
Cargo Build - Inclusion
Clause - Lean
Options - Lean
Scenario Options - The inputs a proof scenario resolves for the Lean backend, carried
through the
__jsonre-entry rather than argv: verbatim argument arrays (no shell splitting), the compiled item selection, and the package-layout overrides. Empty on flag-drivenintoinvocations. - Namespace
- ProVerif
Options - Translation
Options
Enums§
- Backend
- Backend
Name - Command
- Debug
Engine Mode - Deps
Kind - Export
Body Kind - Glob
- Inclusion
Kind - Message
Format - Namespace
Chunk - Path
OrDash - Tools
Command - Subcommands of
cargo hax tools.