Frama-C API - Compute
Used to interpret function calls.
type state = Dom.ttype loc = Loc.locationtype value = Val.tval compute_main_call : Frama_c_kernel.Cil_types.kernel_function -> state -> state Eval.or_bottomAnalysis of a program from the given main function and initial state. Returns the abstract state inferred at the return of the main function.
val compute_call : (loc, value) Eval.call -> Eval.recursion option -> state -> state Engine_sig.call_resultAnalysis 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.