Module Mem_exec

module Mem_exec: sig .. end
This module memorizes the analysis of entire calls to a function, so that those analyzes can be reused later on.

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
Counter that must be used each time a new call is analyzed, in order to refer to it later
module ValueOutputs: Datatype.S  with type t =
  (Cvalue.V_Offsetmap.t option * Cvalue.Model.t) list (** states *) *
  Base.SetLattice.t
Subtype of 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 calls
val 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
Clean all previously stored results