module Mem_exec:sig
..end
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
)
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
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 callsexception Result_found of ValueOutputs.t * int
val find_match_in_previous : MapBasesInputsPrevious.t -> Cvalue.Model.t -> unit
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.)