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