Frama-C:
Plug-ins:
Libraries:

Frama-C API - Eva_results

val is_non_terminating_instr : Frama_c_kernel.Cil_types.stmt -> bool

Returns true iff there exists executions of the statement that does not always fail/loop (for function calls). Must be called *only* on statements that are instructions.

val get_initial_state : unit -> Frama_c_kernel.Cvalue.Model.t option

Returns the initial state provided by set_initial_state below, if any.

val get_main_args : unit -> Frama_c_kernel.Cvalue.V.t list option

Returns the values of the main arguments provided by set_main_args below, if any.

Internal temporary API: please do not use it, as it should be removed in a future version.

Initial cvalue state

val set_initial_state : Frama_c_kernel.Cvalue.Model.t -> unit

Specifies the initial cvalue state to use.

val use_default_initial_state : unit -> unit

Ignores previous calls to set_initial_state above, and uses the default initial state instead.

val set_main_args : Frama_c_kernel.Cvalue.V.t list -> unit

Specifies the values of the main function arguments. Beware that the analysis fails if the number of given values is different from the number of arguments of the entry point of the analysis.

val use_default_main_args : unit -> unit

Ignores previous calls to set_main_args above, and uses the default main argument values instead.

Results

type results
val get_results : unit -> results
val set_results : results -> unit
val merge : results -> results -> results
val change_callstacks : (Callstack.t -> Callstack.t) -> results -> results

Change the callstacks for the results for which this is meaningful. For technical reasons, the top of the callstack must currently be preserved.