Frama-C:
Plug-ins:
Libraries:

Frama-C API - 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:

  • if false, non-volatile global variables are initialized according to their initializers (zero if no explicit initializer).
  • if true, non-const global variables are initialized at top.
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 : (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.