Module `Eva.Eva_results`Source

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.

val eval_tlval_as_location : 
  ?result:Frama_c_kernel.Cil_types.varinfo ->
  Frama_c_kernel.Cvalue.Model.t ->
  Frama_c_kernel.Cil_types.term ->
  Frama_c_kernel.Locations.location

Install

dune-project
Dependency

Authors

Maintainers

Sources

doc/frama-c-eva.core/Eva/Eva_results/index.html

Module `Eva.Eva_results`Source

Initial cvalue state

Results

package frama-c

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/frama-c-eva.core/Eva/Eva_results/index.html

Module Eva.Eva_resultsSource

Initial cvalue state

Results

dune-project
Dependency

Module `Eva.Eva_results`Source