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 (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-31.0-Gallium.tar.gz

sha256=a94384f00d53791cbb4b4d83ab41607bc71962d42461f02d71116c4ff6dca567

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

Module `Eva.Analysis`Source

val compute : unit -> unit

Computes the Eva analysis, if not already computed, using the entry point of the current project. You may set it with Globals.set_entry_point.

raises Globals.No_such_entry_point
if the entry point is incorrect

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

val is_computed : unit -> bool

Return true iff the Eva analysis has been done.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

val self : Frama_c_kernel.State.t

Internal state of Eva analysis from projects viewpoint.

type computation_state =

| NotComputed
| Computing
| Computed
| Aborted
(*
Computation state of the analysis.
*)

val current_computation_state : unit -> computation_state

Get the current computation state of the analysis, updated by force_compute and states updates.

val register_computation_hook : 
  ?on:computation_state ->
  (computation_state -> unit) ->
  unit

Registers a hook that will be called each time the analysis starts or finishes. If on is given, the hook will only be called when the analysis switches to this specific state.

val emitter : Frama_c_kernel.Emitter.t

Emitter used by Eva to emit property statuses.

type results =

| Complete
(*
The results are complete: they cover all possible call contexts of the given function.
*)
| Partial
(*
The results are partial, as the functions has not been analyzed in all possible call contexts. This happens for recursive functions that are not completely unrolled, or if the analysis has stopped unexpectedly.
*)
| NoResults
(*
No results were saved for the function, due to option -eva-no-results. Any request at a statement of this function will lead to a Top result.
*)

Kind of results for the analysis of a function body.

type status =

| Unreachable
(*
The function has not been reached by the analysis. Any request in this function will lead to a Bottom result.
*)
| SpecUsed
(*
The function specification has been used to interpret its calls: its body has not been analyzed. Any request at a statement of this function will lead to a Bottom result.
*)
| Builtin of string
(*
The builtin of the given name has been used to interpret the function: its body has not been analyzed. Any request at a statement of this function will lead to a Bottom result.
*)
| Analyzed of results
(*
The function body has been analyzed.
*)

val status : Frama_c_kernel.Cil_types.kernel_function -> status

Returns the analysis status of a given function.

val use_spec_instead_of_definition : 
  Frama_c_kernel.Cil_types.kernel_function ->
  bool

Does the analysis ignores the body of a given function, and uses instead its specification or a builtin to interpret it? Please use Eva.Results.are_available instead to known whether results are available for a given function.

val save_results : Frama_c_kernel.Cil_types.kernel_function -> bool

Returns true if the user has requested that no results should be recorded for the given function. Please use Eva.Results.are_available instead to known whether results are available for a given function.