package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type
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

  • raises Db.Value.Incorrect_number_of_arguments

    if some arguments are specified for the entry point using Db.Value.fun_set_args, and an incorrect number of them is given.

val is_computed : unit -> bool

Return true iff the Eva analysis has been done.

Internal state of Eva analysis from projects viewpoint.

type computation_state =
  1. | NotComputed
  2. | Computing
  3. | Computed
  4. | 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.

Emitter used by Eva to emit property statuses.

type results =
  1. | Complete
    (*

    The results are complete: they cover all possible call contexts of the given function.

    *)
  2. | 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.

    *)
  3. | 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 =
  1. | Unreachable
    (*

    The function has not been reached by the analysis. Any request in this function will lead to a Bottom result.

    *)
  2. | 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.

    *)
  3. | 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.

    *)
  4. | Analyzed of results
    (*

    The function body has been analyzed.

    *)

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.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct