Module Eva.Eva_resultsSource

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.