package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (23)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-29.0-Copper.tar.gz

sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

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

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

On This Page

Initial cvalue state
Results