Frama-C:
Plug-ins:
Libraries:

Frama-C API - Initialization

type state = Dom.t
val initial_state_with_formals : ?cvalue_state:Frama_c_kernel.Cvalue.Model.t -> ?arguments:Frama_c_kernel.Cvalue.V.t list -> lib_entry:bool -> Frama_c_kernel.Cil_types.kernel_function -> state Eval.or_bottom

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

  • parameter cvalue_state

    if given, replace the computed initial cvalue state with this one.

  • parameter arguments

    if given, use these arguments values instead of generating ad hoc values.

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.