Frama-C:
Plug-ins:
Libraries:

Frama-C API - Make

Parameters

Signature

type state = Engine.Dom.t
val initial_state_with_formals : lib_entry:bool -> Frama_c_kernel.Cil_types.kernel_function -> state Eval.or_bottom

Compute the initial state for an analysis (as in initial_state), but also bind the formal parameters of the function given as argument.

val initialize_local_variable : pos:Position.t -> Eva_ast_types.varinfo -> Eva_ast_types.init -> state -> state Eval.or_bottom

Initializes a local variable in the current state.