Frama-C API - `Eva`

module Abstract : sig ... end

Internal and External signature of abstractions used in the Eva engine.

module Abstract_context : sig ... end

An abstract context can be used to transfer information from the state of an abstract domain, in which an expression or lvalue is evaluated, to a value abstraction, which interprets operations during this evaluation. The context is built by the function build_context of abstract domains, and passed as argument of most transfer functions from Abstract_value.

module Abstract_domain : sig ... end

Abstract domains of the analysis.

module Abstract_location : sig ... end

Abstract memory locations of the analysis.

module Abstract_memory : sig ... end

module Abstract_offset : sig ... end

module Abstract_structure : sig ... end

module Abstract_value : sig ... end

Abstract numeric values of the analysis.

module Abstractions : sig ... end

module Active_behaviors : sig ... end

module Alarmset : sig ... end

Map from alarms to status. Returned by the abstract semantics to report the possible undefined behaviors.

module Analysis : sig ... end

module Analysis_requests : sig ... end

module Assigns : sig ... end

Datastructures and common operations for the results of the From plugin.

module Ast_requests : sig ... end

Requests registered to the Frama-C server; nothing is exported.

module Auto_loop_unroll : sig ... end

Heuristic for automatic loop unrolling.

module Backward_formals : sig ... end

Functions related to the backward propagation of the value of formals at the end of a call. When possible, this value is propagated to the actual parameter.

module Builtins : sig ... end

Eva analysis builtins for the cvalue domain, more efficient than their equivalent in C.

module Builtins_float : sig ... end

Builtins for standard floating-point functions.

module Builtins_malloc : sig ... end

Dynamic allocation related builtins. Most functionality is exported as builtins.

module Builtins_memory : sig ... end

Nothing is exported, all the builtins are registered through Builtins.register_builtin

module Builtins_misc : sig ... end

Builtins for normalization and dumping of values or state. Builtins are registered directly, and are not exported here.

module Builtins_split : sig ... end

module Builtins_string : sig ... end

module Builtins_watchpoint : sig ... end

module Callstack : sig ... end

module Compute_functions : sig ... end

Value analysis of entire functions, using Eva engine.

module Concurrency : sig ... end

module Context_product : sig ... end

Cartesian product of two context abstractions.

module Cvalue_backward : sig ... end

Abstract reductions on Cvalue.V.t

module Cvalue_callbacks : sig ... end

Register actions to performed during the Eva analysis, with access to the states of the cvalue domain. This API is for internal use only, and may be modified or removed in a future version. Please contact us if you need to register callbacks to be executed during an Eva analysis.

module Cvalue_domain : sig ... end

Main domain of the Value Analysis.

module Cvalue_forward : sig ... end

Forward operations on Cvalue.V.t

module Cvalue_init : sig ... end

module Cvalue_offsetmap : sig ... end

Auxiliary functions on cvalue offsetmaps, used by the cvalue domain.

module Cvalue_queries : sig ... end

module Cvalue_results : sig ... end

module Cvalue_transfer : sig ... end

Transfer functions for the main domain of the Value analysis.

module Deps : sig ... end

module Domain_builder : sig ... end

Automatic builders to complete abstract domains from different simplified interfaces.

module Domain_lift : sig ... end

module Domain_mode : sig ... end

This module defines the mode to restrict an abstract domain on specific functions.

module Domain_product : sig ... end

module Domain_store : sig ... end

module Engine : sig ... end

module Engine_abstractions_sig : sig ... end

Signature of abstractions used in the Eva engine.

module Engine_sig : sig ... end

module Equality : sig ... end

Equalities between syntactic lvalues and expressions.

module Equality_domain : sig ... end

module Eva_annotations : sig ... end

module Eva_ast : sig ... end

Eva Syntax Tree.

module Eva_ast_builder : sig ... end

module Eva_ast_datatype : sig ... end

module Eva_ast_deps : sig ... end

Dependencies of expressions and lvalues.

module Eva_ast_printer : sig ... end

module Eva_ast_types : sig ... end

Types definition of the Eva AST for lvalues and expressions. Should also include ACSL terms and predicates in the future. Most types are similar to Cil_types.

module Eva_ast_typing : sig ... end

module Eva_ast_utils : sig ... end

Utilitary functions on the Eva AST of lvalues and expressions.

module Eva_ast_visitor : sig ... end

Rewriting visitor

module Eva_audit : sig ... end

module Eva_automata : sig ... end

Eva automata are Interpreted_automata where transitions have been translated to the Eva AST and where useless transitions have been replaced by Skip. As such, it essentially differs by its simpler vertex, edge and transitions types.

module Eva_dynamic : sig ... end

Access to other plugins API via Dynamic.get.

module Eva_perf : sig ... end

module Eva_results : sig ... end

module Eva_utils : sig ... end

module Eval : sig ... end

module Eval_annots : sig ... end

module Eval_op : sig ... end

Numeric evaluation. Factored with evaluation in the logic.

module Eval_terms : sig ... end

Evaluation of terms and predicates

module Eval_typ : sig ... end

Functions related to type conversions

module Evaluation : sig ... end

module Evaluation_sig : sig ... end

Generic evaluation and reduction of expressions and left values.

module Export : sig ... end

module Field_interval : sig ... end

module Function_calls : sig ... end

module Gauges_domain : sig ... end

Gauges domain ("Arnaud Venet: The Gauge Domain: Scalable Analysis of Linear Inequality Invariants. CAV 2012")

module Hcexprs : sig ... end

Hash-consed expressions and lvalues.

module IEEE754 : sig ... end

The goal of this module is to provide a way to build a sound overapproximation of the semantics of IEEE-754 correctly rounded operations for floating-point formats supported by the C language.

module IEEE754_sig : sig ... end

This module provides the type definitions and module signatures used by the IEEE754 module to build an abstract semantics of floating-point computations as defined by the IEEE-754 standard. See this module for more information.

module Initialization : sig ... end

Creation of the initial state of abstract domain.

module Inout_access : sig ... end

Read and written memory zones at some given Position.t point.

module Inout_domain : sig ... end

Computation of inputs of outputs.

module Interferences : sig ... end

module Iterator : sig ... end

module Library_functions : sig ... end

module Locals_scoping : sig ... end

Auxiliary functions to mark invalid (more precisely 'escaping') the references to a variable whose scope ends.

module Location_lift : sig ... end

module Locations_product : sig ... end

module Logic_inout : sig ... end

Functions used by the Inout and From plugins to interpret predicate and assigns clauses. This API may change according to these plugins development.

module Main_locations : sig ... end

Main memory locations of Eva that can be used by abstract domains.

module Main_values : sig ... end

Main numeric values of Eva that can be used by abstract domains.

module Mem_exec : sig ... end

module Mqueue : sig ... end

module Mt_domain : sig ... end

module Mt_mutex : sig ... end

module Mt_register : sig ... end

module Mt_thread : sig ... end

module Mt_utils : sig ... end

module Multidim : sig ... end

module Multidim_domain : sig ... end

module Mutex : sig ... end

module Octagons : sig ... end

module Offsm_domain : sig ... end

module Offsm_value : sig ... end

module Parameters : sig ... end

module Partition : sig ... end

A partition is a collection of states, each identified by a unique key. The keys define the states partition: states with identical keys are joined together, while states with different keys are maintained separate. A key contains the reason for which a state must be kept separate from others, or joined with similar states.

module Partitioning_index : sig ... end

A partitioning index is a collection of states optimized to determine if a new state is included in one of the states it contains — in a more efficient way than to test the inclusion with all stored states. Such an index is used to keep track of all the states already propagated through a control point, and to rule out new incoming states included in previous ones.

module Partitioning_parameters : sig ... end

module Per_stmt_slevel : sig ... end

Fine-tuning for slevel, according to //@ slevel directives.

module Position : sig ... end

Description of the current position of the analysis.

module Pretty_memory : sig ... end

module Printer_domain : sig ... end

module Private : sig ... end

For internal use only: optional domains (numerors and apron) are compiled separately from the Eva core. This is used to give them access to the internal modules of Eva they need.

module Recursion : sig ... end

Handling of recursion cycles in the callgraph

module Red_statuses : sig ... end

This modules stores the alarms and properties for which a red status has been emitted.

module Results : sig ... end

Eva's result API is a new interface to access the results of an analysis, once it is completed. It may slightly change in the future.

module Segmentation : sig ... end

module Self : sig ... end

module Sign_domain : sig ... end

Abstraction of the sign of integer variables.

module Sign_value : sig ... end

Sign domain: abstraction of integer numerical values by their signs.

module Simple_memory : sig ... end

Simple memory abstraction for scalar non-volatile variables, built upon a value abstraction. Basically a map from variable to values.

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. More documentation can be found on the complete interface of abstract domains, in Abstract_domain.

module Split_return : sig ... end

This module is used to merge together the final states of a function according to a given strategy. Default is to merge all states together

module Split_strategy : sig ... end

module Statistics : sig ... end

module Stats_requests : sig ... end

Requests registered to the Frama-C server; nothing is exported.

module Structure : sig ... end

Gadt describing the structure of a tree of different data types, and providing fast accessors of its nodes. The leaves must provide a key from a Key module, see key.mli for details.

module Subdivided_evaluation : sig ... end

Subdivision of the evaluation on non-linear expressions: for expressions in which some l-values appear multiple times, proceed by disjunction on their abstract value, in order to gain precision.

module Summary : sig ... end

module Symbolic_locs : sig ... end

Domain that store information on non-precise l-values such as t[i] or *p when i or p is not exact.

module Taint_domain : sig ... end

Domain for a taint analysis.

module Taint_requests : sig ... end

module Thread : sig ... end

module Trace_partitioning : sig ... end

module Traces_domain : sig ... end

module Transfer_inout : sig ... end

Helper module to register read and written memory zones to Inout_access in Transfer_stmt and Transfer_specification

module Transfer_logic : sig ... end

module Transfer_specification : sig ... end

Interpretation of function specification.

module Transfer_stmt : sig ... end

module Typed_memory : sig ... end

module Unit_context : sig ... end

module Unit_domain : sig ... end

module Unit_tests : sig ... end

Currently tested by this module:

module Value_lift : sig ... end

module Value_product : sig ... end

Cartesian product of two value abstractions.

module Value_requests : sig ... end

Requests registered to the Frama-C server; nothing is exported.

module Widen : sig ... end

Per-function computation of widening hints.

module Widen_hints_ext : sig ... end

Syntax extension for widening hints, used by Value.

Frama-C API - Eva

Frama-C API - `Eva`