X.Compute
type state = Dom.t
type loc = Loc.location
type value = Val.t
val compute_from_entry_point :
Frama_c_kernel.Cil_types.kernel_function ->
lib_entry:bool ->
unit
Analysis of a program from the given main function. Computed states for each statement are stored in the result tables of each enabled abstract domain. This is called by Analysis.compute
. The initial abstract state is computed according to lib_entry
:
val compute_from_init_state :
Frama_c_kernel.Cil_types.kernel_function ->
state ->
unit
Analysis of a program from the given main function and initial state.
val compute_call :
Frama_c_kernel.Cil_types.stmt ->
(loc, value) Eva.Eval.call ->
Eva.Eval.recursion option ->
state ->
state Eva__.Engine_sig.call_result
Analysis of a function call during the Eva analysis. This function is called by Transfer_stmt
when interpreting a call statement. compute_call stmt call recursion state
analyzes the call call
at statement stmt
in the input abstract state state
. If recursion
is not None
, the call is a recursive call.