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

Functions of the Value plugin registered in Db.

Value_parameters

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 Api (in value/api)


General_requests

General Eva requests registered in the server.

Values_request

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
Powerset
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
Compute_functions

Value analysis of entire functions, using Eva engine.

Evaluation
Initialization

Creation of the initial state of abstract domain.

Iterator
Mem_exec
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
Transfer_specification
Transfer_stmt

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

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
Library_functions
Mark_noresults
Red_statuses
Structure

Gadt describing the structure of a tree of different data types, and providing fast accessors of its nodes.

Unit_tests

Currently tested by this file: semantics of sign values.

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
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
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
Numerors_float
Numerors_interval
Numerors_utils
Numerors_value