Module Analysis

module Analysis: sig .. end

module type Results = sig .. end

module Make: functor (Abstract : Abstractions.S) -> sig .. end

module type S = sig .. end

val current_analyzer : unit -> (module Analysis.S)

The abstractions used in the latest analysis, and its results.

val register_hook : ((module Analysis.S) -> unit) -> unit

Registers a hook that will be called each time the current analyzer is changed. This happens when a new analysis is run with different abstractions than before, or when the current project is changed.

val force_compute : unit -> unit

Perform a full analysis, starting from the main function.

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
- 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.

Consult the Plugin Development Guide

val is_computed : unit -> bool

Return true iff the Eva analysis has been done.

Consult the Plugin Development Guide

val self : 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.

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 : Cil_types.kernel_function -> status

Returns the analysis status of a given function.

val use_spec_instead_of_definition : 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 : 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.

val cvalue_initial_state : unit -> Cvalue.Model.t

Return the initial state of the cvalue domain only.