Global config
val under_approximation : bool Stdlib.refval results_dir : unit -> stringval set_result_dir : string -> unitval entry_point : string Stdlib.refval json_ui : bool Stdlib.refval previously_normalised : bool Stdlib.refval unfolding : bool Stdlib.refval manual_proof : bool Stdlib.refval max_branching : int Stdlib.refval leak_check : bool Stdlib.refval lemma_proof : bool Stdlib.refval dump_annots : bool Stdlib.refval debug_log_verbose : bool Stdlib.refHashtable sizes
val medium_tbl_size : intBi-abduction config
These values seem to never be modified
val specs_to_stdout : bool Stdlib.refDebugging config
val debug : bool Stdlib.refWhether Gillian is running in debugger mode
Printing config
val no_heap : bool Stdlib.refLimited printing
val pbn : bool Stdlib.refStatistics
val stats : bool Stdlib.refSymbolic execution
TODO: This should have a better name.
val bi_dflt : bool Stdlib.refval bi_unfold_depth : int Stdlib.refval bi_unroll_depth : int Stdlib.refval bi_no_spec_depth : int Stdlib.refval delay_entailment : bool Stdlib.refval dump_smt : bool Stdlib.refBulk testing
val bulk_print_all_failures : bool Stdlib.refIf 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 -> unitval get_runtime_paths : unit -> string list