Module Soteria_rust_lib.Config

type frontend =
  1. | Charon
  2. | Obol
val frontend_cmdliner_conv : unit -> frontend Cmdliner.Arg.conv
val pp_frontend : Ppx_deriving_runtime.Format.formatter -> frontend -> Ppx_deriving_runtime.unit
val show_frontend : frontend -> Ppx_deriving_runtime.string
type provenance =
  1. | Strict
  2. | Permissive
val provenance_cmdliner_conv : unit -> provenance Cmdliner.Arg.conv
type check_level =
  1. | Deny
  2. | Warn
  3. | Allow
val check_level_cmdliner_conv : unit -> check_level Cmdliner.Arg.conv
type t = {
  1. cleanup : bool;
    (*

    Clean up compiled files after execution

    *)
  2. log_compilation : bool;
    (*

    Log the compilation process

    *)
  3. no_compile : bool;
    (*

    Do not compile the Rust code, as it is already compiled

    *)
  4. no_compile_plugins : bool;
    (*

    Do not compile the plugins, as they are already compiled

    *)
  5. plugin_directory : string option;
    (*

    The directory in which plugins are and should be compiled; defaults to the current dune-managed site.

    *)
  6. target : string option;
    (*

    The compilation target triple to use, e.g. x86_64-unknown-linux-gnu. If not provided, the default target for the current machine is used.

    *)
  7. polymorphic : bool;
    (*

    Whether compilation (and thus analysis) should be done on polymorphic code (experimental), rather than on monomorphic code (with generics substituted).

    *)
  8. output_crate : bool;
    (*

    Pretty-print the compiled crate to a file

    *)
  9. rustc_flags : string list;
    (*

    Additional flags to pass to the Rustc compiler

    *)
  10. frontend : frontend;
    (*

    Choose the frontend to use: Charon or Obol

    *)
  11. obol_path : string;
    (*

    Path to the obol binary. Defaults to "obol", i.e. looked up in PATH.

    *)
  12. charon_path : string;
    (*

    Path to the charon binary. Defaults to "charon", i.e. looked up in PATH.

    *)
  13. sysroot : string option;
    (*

    The sysroot to use for compilation. If not provided, the default sysroot is used.

    *)
  14. test : string option;
    (*

    The test profile to use to compile the crate; this only has an effect if analysing a crate. By default, the crate's source is analysed, not the tests.

    *)
  15. with_kani : bool;
    (*

    Use the Kani library

    *)
  16. with_miri : bool;
    (*

    Use the Miri library

    *)
  17. filter : Str.regexp list;
    (*

    Filter the entrypoints to run, by name. If empty, all entrypoints are run. Multiple filters can be provided, comma-separated; tests matching any will be selected. The filters are treated as regexes. Opposite of --exclude.

    *)
  18. exclude : Str.regexp list;
    (*

    Filter the entrypoints to exclude, by name. If empty, no entrypoints are excluded. Multiple filters can be provided, comma-separated; tests matching any will be excluded. The filters are treated as regexes. Opposite of --filter.

    *)
  19. print_summary : bool;
    (*

    If a summary of all test cases should be printed at the end of execution

    *)
  20. show_pcs : bool;
    (*

    Whether to show the path conditions for outcomes at the end of execution.

    *)
  21. ignore_leaks : bool;
    (*

    Ignore memory leaks

    *)
  22. ignore_aliasing : bool;
    (*

    Ignore pointer aliasing rules (tree borrows)

    *)
  23. provenance : provenance;
    (*

    The provenance model to use for pointers. If not provided, the default is permissive.

    *)
  24. recursive_validity : check_level;
    (*

    Whether to check the validity of the addressed memory when obtaining a reference to it. We only go one level deep.

    *)
  25. approx_floating_ops : check_level;
    (*

    Whether to allow complex floating-point operations to be over-approximated. Applies to e.g. sqrt, exp, pow and trigonometric functions. If deny, will vanish execution when encountering them.

    *)
  26. step_fuel : int option;
    (*

    The default step fuel for each entrypoint -- every control flow jump counts as one fuel. Defaults to infinite fuel.

    *)
  27. branch_fuel : int option;
    (*

    The default branch fuel for each entrypoint -- every symbolic execution branching point counts as one fuel. Defaults to infinite fuel.

    *)
  28. fail_fast : bool;
    (*

    Stop symbolic execution upon the first error encountered.

    *)
}
val make : ?cleanup:bool -> ?log_compilation:bool -> ?no_compile:bool -> ?no_compile_plugins:bool -> ?plugin_directory:string -> ?target:string -> ?polymorphic:bool -> ?output_crate:bool -> ?rustc_flags:string list -> ?frontend:frontend -> ?obol_path:string -> ?charon_path:string -> ?sysroot:string -> ?test:string -> ?with_kani:bool -> ?with_miri:bool -> ?filter:Str.regexp list -> ?exclude:Str.regexp list -> ?print_summary:bool -> ?show_pcs:bool -> ?ignore_leaks:bool -> ?ignore_aliasing:bool -> ?provenance:provenance -> ?recursive_validity:check_level -> ?approx_floating_ops:check_level -> ?step_fuel:int -> ?branch_fuel:int -> ?fail_fast:bool -> unit -> t
val cmdliner_term : unit -> t Cmdliner.Term.t
type mode =
  1. | Compositional
  2. | Whole_program
val term : t Cmdliner.Term.t
val default : t
val get : unit -> t
val set_and_lock : t -> unit
val get_mode : unit -> mode
val set_mode_and_lock : mode -> unit
type global = {
  1. soteria : Soteria.Config.t;
  2. soteria_rust : t;
}
val make_global : soteria:Soteria.Config.t -> soteria_rust:t -> global
val global_cmdliner_term : unit -> global Cmdliner.Term.t
val global_term : global Cmdliner.Term.t
val set_and_lock_global : mode -> global -> unit