Config (gillian.Utils.Config)

val under_approximation : bool Stdlib.ref

val results_dir : unit -> string

val set_result_dir : string -> unit

val entry_point : string Stdlib.ref

val json_ui : bool Stdlib.ref

val ci : bool Stdlib.ref

val current_exec_mode : Exec_mode.t Stdlib.ref

val previously_normalised : bool Stdlib.ref

val unfolding : bool Stdlib.ref

val manual_proof : bool Stdlib.ref

val max_branching : int Stdlib.ref

val leak_check : bool Stdlib.ref

val lemma_proof : bool Stdlib.ref

val dump_annots : bool Stdlib.ref

val debug_log_verbose : bool Stdlib.ref

val small_tbl_size : int

val medium_tbl_size : int

val big_tbl_size : int

These values seem to never be modified

val specs_to_stdout : bool Stdlib.ref

val debug : bool Stdlib.ref

Whether Gillian is running in debugger mode

val no_heap : bool Stdlib.ref

val pbn : bool Stdlib.ref

val stats : bool Stdlib.ref

TODO: This should have a better name.

val bi_dflt : bool Stdlib.ref

val bi_unfold_depth : int Stdlib.ref

val bi_unroll_depth : int Stdlib.ref

val bi_no_spec_depth : int Stdlib.ref

val delay_entailment : bool Stdlib.ref

val dump_smt : bool Stdlib.ref

val bulk_print_all_failures : bool Stdlib.ref

If activated, at the end of bulk execution or bulk wpst, and only with the Rely runner, a list of all failures will be printed in stdout

val set_runtime_paths : ?default_folders:string list -> string list -> unit

val get_runtime_paths : unit -> string list

module Verification = Gillian.Utils.Config.Verification