Module Self

module Self: sig .. end

include Plugin.General_services
val proxy : State_builder.Proxy.t
val state : State.t
val is_computed : unit -> bool

Return true iff the value analysis has been done.

type computation_state = 
| NotComputed
| Computing
| Computed
| Aborted

Computation state of the analysis.

val current_computation_state : unit -> computation_state

Get the current computation state of the analysis, updated by force_compute and states updates.

val set_computation_state : computation_state -> unit

Set the current computation state.

val register_computation_hook : ?on:computation_state -> (computation_state -> unit) -> unit

Registers a hook that will be called each time the analysis starts or finishes. If on is given, the hook will only be called when the analysis switches to this specific state.

val dkey_initial_state : category

Debug categories responsible for printing initial and final states of Value. Enabled by default, but can be disabled via the command-line: -value-msg-key="-initial_state,-final_state"

val dkey_final_states : category
val dkey_summary : category

Debug categories.

val dkey_pointer_comparison : category
val dkey_cvalue_domain : category
val dkey_incompatible_states : category
val dkey_iterator : category
val dkey_callbacks : category
val dkey_widening : category
val dkey_recursion : category

Warning categories.

val wkey_alarm : warn_category
val wkey_locals_escaping : warn_category
val wkey_garbled_mix : warn_category
val wkey_builtins_missing_spec : warn_category
val wkey_builtins_override : warn_category
val wkey_libc_unsupported_spec : warn_category
val wkey_loop_unroll_auto : warn_category
val wkey_loop_unroll_partial : warn_category
val wkey_missing_loop_unroll : warn_category
val wkey_missing_loop_unroll_for : warn_category
val wkey_signed_overflow : warn_category
val wkey_invalid_assigns : warn_category
val wkey_experimental : warn_category
val wkey_unknown_size : warn_category
val wkey_ensures_false : warn_category