Frama-C API - `Eva`

Eva public API.

Apart from Analysis and Results, all modules exported here are development interfaces which may change with each Frama-C release.

Main stable API

module Analysis : sig ... end

Run the analysis and check analysis status.

module Results : sig ... end

Main API to access the results of an analysis, such as the possible values of expressions and memory locations of lvalues at each program point.

Statistics

module Eva_perf : sig ... end

Statistics about the analysis performance.

module Statistics : sig ... end

Various statistics collected during an analysis.

Types used in Eva

module Eva_ast : sig ... end

AST used by Eva.

module Position : sig ... end

Position in the analysis

module Callstack : sig ... end

Types of callstack.

module Deps : sig ... end

Types for the memory dependencies of an expression or lvalue.

Configuration of the analysis

module Parameters : sig ... end

Command-line parameters of the analysis.

module Eva_annotations : sig ... end

Add local annotations to guide the analysis.

module Builtins : sig ... end

Registration of new abstractions

module Eval : sig ... end

Various types used in abstract domain signature.

module Abstract_domain : sig ... end

Signature of abstract domains, inferring properties about the program during the analysis.

module Abstract_value : sig ... end

Signature of abstract numerical values, representing the set of possible values of an expression or lvalue. Used to exchange information between abstract domains.

module Abstract_location : sig ... end

Signature of abstract memory locations, representing the set of possible memory locations pointed to by an lvalue.

module Abstract_context : sig ... end

Signature of abstract state, which can be used to transfer information from states of abstract domains to abstract values.

module Unit_context : sig ... end

Empty context.

module Domain_builder : sig ... end

Automatic builders to complete abstract domains from different simplified interfaces.

module Simpler_domains : sig ... end

Simplified interfaces for abstract domains. Complete abstract domains can be built from these interfaces through the functors in Domain_builder.

module Simple_memory : sig ... end

Build a domain upon a value abstraction with a very simple memory model for scalar non-volatile variables.

module Domain : sig ... end

module Main_values : sig ... end

Common value abstractions shared by many abstract domains.

module Main_locations : sig ... end

Common location abstractions shared by many abstract domains.

Internal API

These modules are for internal use only. They may be modified or removed in future versions. Please contact us if you need features from these modules.

module Export : sig ... end

Generation of annotations.

module Assigns : sig ... end

Types and operations for the From plugin.

module Cvalue_callbacks : sig ... end

module Logic_inout : sig ... end

Interpretation of predicates and assigns clauses for Inout and From plugins.

module Eva_results : sig ... end

Undocumented.

module Unit_tests : sig ... end

Unit testing.