module Make:
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.)