Functor Mem_exec.Make

module Make: 
functor (Value : Datatype.S) ->
functor (Domain : Domain) -> sig .. end
Parameters:
Value : Datatype.S
Domain : Domain

val store_computed_call : Cil_types.kernel_function ->
Mem_exec.Domain.t ->
Value.t Eval.or_bottom list -> Mem_exec.Domain.t list Eval.or_bottom -> unit
store_computed_call kf init_state args call_results memoizes the fact that calling kf with initial state init_state and arguments args resulted in the results call_results. Those information are intended to be reused in subsequent calls
val reuse_previous_call : Cil_types.kernel_function ->
Mem_exec.Domain.t ->
Value.t Eval.or_bottom list ->
(Mem_exec.Domain.t list Eval.or_bottom * int) option
reuse_previous_call kf init_state args searches amongst the previous analyzes of kf one that matches the initial state init_state and the values of arguments args. 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.)