Module Codex_config

module Log : Tracelog.S

Domains options

val r_ptr_size : Units.In_bits.t Stdlib.ref
val set_ptr_size : Units.In_bits.t -> unit
val ptr_size : unit -> Units.In_bits.t
val function_size : unit -> int
val back_propagation_limit : int Stdlib.ref

Limit the number of backpropagations performed in non-relational domains

val set_back_propagation_limit : int -> unit
val get_back_propagation_limit : unit -> int
val terms_register_parents : unit -> bool
val array_expansion : unit -> [ `full_expansion | `full_squashing ]

Term generation options.

val assume_alarms : unit -> bool
val translation_to_smt_use_integer : unit -> bool

Debugging options

val print_smt_input : unit -> bool

Goal-oriented options

val try_hard_with_deductive_verification : unit -> bool
val try_hard_with_symbolic_execution : unit -> bool
val try_hard_with_muz : unit -> bool
val muz_engine : unit -> string
val try_hard_double_check : unit -> bool
val smt_timeout : unit -> int
val term_group_inductive_variable_by_tuple : bool
val r_valid_absolute_addresses : (Z.t * Z.t) option Stdlib.ref
val set_valid_absolute_addresses : (Z.t * Z.t) -> unit
val valid_absolute_addresses : unit -> (Z.t * Z.t) option
val r_show_memory_on_exit : bool Stdlib.ref
val show_memory_on_exit : unit -> bool
val set_show_memory_on_exit : bool -> unit
val r_assume_simple_asts : bool Stdlib.ref
val set_assume_simple_asts : bool -> unit
val assume_simple_asts : unit -> bool
val widen : unit -> bool
val handle_malloc_as_unknown_typed_pointers : unit -> bool
val hash_cons_terms_with_weak_table : unit -> bool
val extend_size_for_additive_operations : Units.In_bits.t -> Units.In_bits.t