Frama-C API - Compute
Complete analysis of functions, built by the functor Compute_functions.Make.
val 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 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.