Eva plugin


Directory domains

Section Apron (in domains/apron)


Apron_domain
Experimental binding for the numerical abstract domains provided by the APRON library: http://apron.cri.ensmp.fr/library For now, this binding only processes scalar integer variables.

Section Cvalue (in domains/cvalue)


Builtins
Value analysis builtin shipped with Frama-C, more efficient than their equivalent in C
Builtins_float
Builtins for standard floating-point functions.
Builtins_malloc
Dynamic allocation related builtins.
Builtins_memory
Nothing is exported, all the builtins are registered through
Builtins_misc
Builtins for normalization and dumping of values or state.
Builtins_print_c
Translate a Value state into a bunch of C assertions
Builtins_split
Enumeration
Builtins_string
A builtin takes the state and a list of values for the arguments, and returns the offsetmap of the return value (None if bottom), and a boolean indicating the possibility of alarms.
Builtins_watchpoint
Cvalue_domain
Main domain of the Value Analysis.
Cvalue_init
Creation of the initial state for Value
Cvalue_offsetmap
Auxiliary functions on cvalue offsetmaps, used by the cvalue domain.
Cvalue_specification
No function exported.
Cvalue_transfer
Transfer functions for the main domain of the Value analysis.
Locals_scoping
Auxiliary functions to mark invalid (more precisely 'escaping') the references to a variable whose scope ends.
Warn
Alarms and imprecision warnings emitted during the analysis.

Section Equality (in domains/equality)


Equality
Equalities between syntactic lvalues and expressions.
Equality_domain
Initial abstract state at the beginning of a call.

Section Gauges (in domains/gauges)


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

Section Numerors (in domains/numerors)


Numerors_domain
Numerors domain: computes over-approximations of the rounding errors bounds of floating-point computations.

Directory plugins

Section Value (in plugins/value)


Alarmset
Map from alarms to status.
Eva
Analysis for values and pointers
Eval
Types and functions related to evaluations.
Register
Functions of the Value plugin registered in Db.
Value_parameters
Dynamic allocation

Section Value_types (in plugins/value_types)


CilE
Value analysis alarms
Cvalue
Representation of Value's abstract memory.
Precise_locs
This module provides transient datastructures that may be more precise than an Ival.t, Locations.Location_Bits.t and Locations.location respectively, typically for l-values such as t[i][j], p->t[i], etc.
Value_types
Declarations that are useful for plugins written on top of the results of Value.
Widen_type
Widening hints for the Value Analysis datastructures.

Directory value

Section Domains (in value/domains)


Abstract_domain
Abstract domains of the analysis.
Domain_builder
Automatic builders to complete abstract domains from different simplified interfaces.
Domain_lift
Domain_mode
This module defines the mode to restrict an abstract domain on specific functions.
Domain_product
Domain_store
Hcexprs
Hash-consed expressions and lvalues.
Inout_domain
Computation of inputs of outputs.
Octagons
Offsm_domain
If true, the offsetmap domain stores information that can probably be re-synthesized from the value domain.
Powerset
Set of states, propagated through the edges by the dataflow analysis.
Printer_domain
An abstract domain built on top of the Simpler_domains.Simple_Cvalue interface that just prints the transfer functions called by the engine during an analysis.
Sign_domain
Abstraction of the sign of integer variables.
Simple_memory
Simple memory abstraction for scalar non-volatile variables, built upon a value abstraction.
Simpler_domains
Simplified interfaces for abstract domains.
Symbolic_locs
Domain that store information on non-precise l-values such as t[i] or *p when i or p is not exact.
Traces_domain
Traces domain
Unit_domain

Section Engine (in value/engine)


Abstractions
Registration and building of the analysis abstractions.
Analysis
The abstractions used in the latest analysis, and its results.
Compute_functions
Value analysis of entire functions, using Eva engine.
Evaluation
Generic evaluation and reduction of expressions and left values.
Initialization
Creation of the initial state of abstract domain.
Iterator
Mark the analysis as aborted.
Mem_exec
Counter that must be used each time a new call is analyzed, in order to refer to it later
Recursion
Handling of recursion cycles in the callgraph
Subdivided_evaluation
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.
Transfer_logic
Check the postcondition of kf for the list of behaviors.
Transfer_specification
Transfer_stmt
Applies the show_each or dump_each directives.

Section Gui_files (in value/gui_files)


Gui_callstacks_filters
Filtering on analysis callstacks
Gui_callstacks_manager
This module creates and manages the "Values" panel on the lower notebook of the GUI.
Gui_eval
This module defines an abstraction to evaluate various things across multiple callstacks.
Gui_red
Extension of the GUI in order to display red alarms emitted during the value analysis
Gui_types
The types below depend on the abstract values currently available.
Register_gui
Extension of the GUI in order to support the value analysis.

Section Legacy (in value/legacy)


Eval_annots
Eval_op
Numeric evaluation.
Eval_terms
Evaluation of terms and predicates
Function_args
Nothing is exported; the function compute_atual is registered in Db.Value.

Section Partitioning (in value/partitioning)


Auto_loop_unroll
Heuristic for automatic loop unrolling.
Partition
A partition is a collection of states, each identified by a unique key.
Partitioning_index
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.
Partitioning_parameters
Per_stmt_slevel
Fine-tuning for slevel, according to //@ slevel directives.
Split_return
This module is used to merge together the final states of a function according to a given strategy.
Split_strategy
Trace_partitioning
The states being partitioned

Section Utils (in value/utils)


Abstract
Internal and External signature of abstractions used in the Eva engine.
Backward_formals
Functions related to the backward propagation of the value of formals at the end of a call.
Eva_annotations
Registers Eva annotations: slevel annotations: "slevel default", "slevel merge" and "slevel i", loop unroll annotations: "loop unroll term", value partitioning annotations: "split term" and "merge term", subdivision annotations: "subdivide i" Widen hints annotations are still registered in !.
Eval_typ
Functions related to type conversions
Library_functions
Fake varinfo used by Value to store the result of functions.
Mark_noresults
Red_statuses
This modules stores the alarms and properties for which a red status has been emitted.
State_import
Saving/loading of Value states, possibly among different ASTs.
Structure
Gadt describing the structure of a tree of different data types, and providing fast accessors of its nodes.
Value_perf
Call start_doing when starting analyzing a new function.
Value_results
This file will ultimately contain all the results computed by Value (which must be moved out of Db.Value), both per stack and globally.
Value_util
Callstacks related types and functions
Widen
Per-function computation of widening hints.
Widen_hints_ext
Syntax extension for widening hints, used by Value.

Section Values (in value/values)


Abstract_location
Abstract memory locations of the analysis.
Abstract_value
Abstract numeric values of the analysis.
Cvalue_backward
Abstract reductions on Cvalue.V.t
Cvalue_forward
Forward operations on Cvalue.V.t
Location_lift
Main_locations
Main memory locations of Eva:
Main_values
Main numeric values of Eva.
Offsm_value
Auxiliary functions
Sign_value
Sign domain: abstraction of integer numerical values by their signs.
Value_product
Cartesian product of two value abstractions.

Directory values

Section Numerors (in values/numerors)


Numerors_arithmetics
Type manipulated by the arithmetics
Numerors_float
Returns a t element representing a positive infinite value
Numerors_interval
Opaque type of an interval.
Numerors_utils
We handle the format defined in C.
Numerors_value
Reduction of an error value according to a floating-point interval.