gillian » Gillian » Utils » Config

Module Utils.Config

Global config

val under_approximation : bool Stdlib.ref

val results_dir : unit -> string

val set_result_dir : string -> unit

val file_content_overrides : (string, string) Stdlib.Hashtbl.t

val entry_point : string Stdlib.ref

val json_ui : bool Stdlib.ref

val ci : bool Stdlib.ref

val current_exec_mode : Utils.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

Hashtable sizes

val small_tbl_size : int

val medium_tbl_size : int

val big_tbl_size : int

Bi-abduction config

These values seem to never be modified

val specs_to_stdout : bool Stdlib.ref

Debugging config

val debug : bool Stdlib.ref

Whether Gillian is running in debugger mode

Printing config

val no_heap : bool Stdlib.ref

Limited printing

val pbn : bool Stdlib.ref

Statistics

val stats : bool Stdlib.ref

Symbolic execution

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

Bulk testing

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

Runtime settings

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

val get_runtime_paths : unit -> string list

module Verification : sig ... end

val reset_config_f : (unit -> unit) option Stdlib.ref

Resetting

With the addition of in-file config statements, we want to be able to "reset" the config when analysis is run multiple times in one "instance", i.e. the LSP.

val reset_config : unit -> unit

val usage_logs : bool Stdlib.ref

val usage_logs_file : string Stdlib.ref

val usage_logs_git_ref : string Stdlib.ref