Functor Mem_exec.Make

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

Parameters:

`Value`	:	`Datatype.S`
`Domain`	:	`Abstract_domain.S`

val store_computed_call : Cil_types.kernel_function ->
       Domain.t ->
       Value.t Eval.or_bottom list -> (Partition.key * Domain.t) list -> 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 ->
       Domain.t ->
       Value.t Eval.or_bottom list -> ((Partition.key * Domain.t) list * 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.)