module Mem_exec:sig
..end
diff_base_full_zone bases zones
remove from the set of bases bases
those of which all bits are present in zones
val new_counter : unit -> int
module ValueOutputs:Datatype.S
with type t = (Cvalue.V_Offsetmap.t option * Cvalue.Model.t) list (** states *) * Base.SetLattice.t
Value_types.call_res
val store_computed_call : Value_types.call_site ->
Cvalue.Model.t ->
(Cil_types.exp * Cvalue.Model.offsetmap) list ->
Value_types.call_result -> unit
store_computed_call (kf, ki) init_state actuals outputs
memoizes the fact
that calling kf
at statement ki
, with initial state init_state
and arguments actuals
resulted in the states outputs
; the expressions
in the actuals are not used. Those information are intended to be reused
in subsequent callsval reuse_previous_call : Value_types.call_site ->
Cvalue.Model.t ->
(Cil_types.exp * Cvalue.Model.offsetmap) list ->
(Value_types.call_result * int) option
reuse_previous_call (kf, ki) init_state
searches amongst the previous
analyzes of kf
one that matches the initial state init_state
. If
none is found, None
is returned. Otherwise, the results of the analysis
are returned, together with the index of the matching call. (This last
information is intended to be used by the plugins that have registered
Value callbacks.)val cleanup_results : unit -> unit