Module Mem_exec

module Mem_exec: sig .. end

Find a previous execution in map_inputs that matches st. raise Result_found when this execution exists, or do nothing.

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

exception TooImprecise

val bases : Locations.Zone.tt -> Base.SetLattice.O.t

val filter_state : Base.Hptset.t -> Cvalue.Model.t -> Cvalue.Model.t

module ValueOutputs: Datatype.Pair(Datatype.List(Datatype.Pair(Datatype.Option(Cvalue.V_Offsetmap))(Cvalue.Model)))(Base.SetLattice)

Subtype of Value_types.call_res

module PreviousState: Datatype.Pair(ValueOutputs)(Datatype.Int)

module Actuals: sig .. end

module ActualsList: Datatype.List_with_collections(Actuals)(sig
val module_name : string
end)

module MapInputsPrevious: Cvalue.Model.Hashtbl.Make(PreviousState)

module MapBasesInputsPrevious: Base.Hptset.Hashtbl.Make(MapInputsPrevious)

module MapActualsBasesInputsPrevious: ActualsList.Map.Make(MapBasesInputsPrevious)

module PreviousStates: State_builder.Hashtbl(Kernel_function.Hashtbl)(MapActualsBasesInputsPrevious)(sig
val size : int
val dependencies : State.t list
val name : string
end)

module ResultFromCallback: State_builder.Option_ref(Datatype.Pair(Value_types.Callstack)(Inout_type))(sig
val dependencies : State.t list
val name : string
end)

val cleanup_results : unit -> unit

Clean all previously stored results

val map_to_outputs : (Cvalue.Model.t -> 'a) ->
       (Cvalue.V_Offsetmap.t option * Cvalue.Model.t) list ->
       (Cvalue.V_Offsetmap.t option * 'a) list

val register_callback : unit -> unit

module SaveCounter: State_builder.SharedCounter(sig
val name : string
end)

val store_computed_call : Value_types.call_site ->
       Cvalue.Model.t ->
       ActualsList.Map.key -> 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

exception Result_found of ValueOutputs.t * int

val find_match_in_previous : MapBasesInputsPrevious.t -> Cvalue.Model.t -> unit

Find a previous execution in map_inputs that matches st. raise Result_found when this execution exists, or do nothing.

val reuse_previous_call : Value_types.call_site ->
       Cvalue.Model.t ->
       ActualsList.Map.key -> (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.)