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.)