Module Soteria_c_lib.Config

type t = {
  1. auto_include_path : string option;
    (*

    Path to the directory that contains the soteria-c.h

    *)
  2. no_ignore_parse_failures : bool;
    (*

    Files that cannot be parsed correctly are ignored by default, this flag deactivates that behaviour.

    *)
  3. no_ignore_duplicate_symbols : bool;
    (*

    Programs that contain duplicate symbols are ignored by default, this flag deactivates that behaviour.

    *)
  4. parse_only : bool;
    (*

    Only parse and link the C program, do not perform analysis

    *)
  5. no_c23 : bool;
    (*

    Disable C23 support (even if the underlying Cerberus library supports it).

    *)
  6. dump_summaries_file : string option;
    (*

    Dump the generated summaries to a file

    *)
  7. show_manifest_summaries : bool;
    (*

    Print a corresponding manifest summary after the bug report if a bug is found

    *)
  8. alloc_cannot_fail : bool;
    (*

    Assume allocations cannot fail

    *)
  9. use_cerb_headers : bool;
    (*

    Use the Cerberus-provided standard headers instead of the system headers.

    *)
  10. cbmc_compat : bool;
    (*

    Enable support for a subset of the __CPROVER_ API.

    *)
  11. testcomp_compat : bool;
    (*

    Enable support for a subset of the testcomp API (e.g., __VERIFIER_nondet_

    *)
  12. ignore_ub : bool;
    (*

    Ignores undefined behaviour branches (mostly for Test-Comp's weird requirements). Branches reaching UB will be dismissed. Only has effect in symbolic testing mode.

    *)
  13. havoc_undefined_funs : bool;
    (*

    Assume that all undefined functions can return any value. Warning: this can lead to unsoundnesses in analyses.

    *)
  14. print_states : bool;
    (*

    Print final program states after whole-program symbolic testing

    *)
  15. write_parsed_db : string option;
    (*

    When using a compilation database, write a filtered version containing only successfully parsed files to the specified path

    *)
  16. dump_report : string option;
    (*

    Write a JSON report of all diagnostics (bugs and errors) to the specified file

    *)
}
val make : ?auto_include_path:string -> ?no_ignore_parse_failures:bool -> ?no_ignore_duplicate_symbols:bool -> ?parse_only:bool -> ?no_c23:bool -> ?dump_summaries_file:string -> ?show_manifest_summaries:bool -> ?alloc_cannot_fail:bool -> ?use_cerb_headers:bool -> ?cbmc_compat:bool -> ?testcomp_compat:bool -> ?ignore_ub:bool -> ?havoc_undefined_funs:bool -> ?print_states:bool -> ?write_parsed_db:string -> ?dump_report:string -> unit -> t
val cmdliner_term : unit -> t Cmdliner.Term.t
type mode =
  1. | Compositional
  2. | Whole_program
type Stdlib.Effect.t +=
  1. | GetConfig : t Stdlib.Effect.t
type Stdlib.Effect.t +=
  1. | GetMode : mode Stdlib.Effect.t
val default : t
val current : unit -> t
val current_mode : unit -> mode
val with_config : config:t -> mode:mode -> (unit -> 'a) -> 'a