Index of modules

A
Abstract_domain

Abstract domains of the analysis.

Abstract_location

Abstract memory locations of the analysis.

Abstract_value

Abstract numeric values of the analysis.

Abstractions

Constructions of the abstractions used by Eva.

ActiveBehaviors [Transfer_logic]
AlarmOrProp [Red_statuses]
AlarmsWarnings [Value_parameters]
Alarmset

Map from alarms to status.

AllRoundingModesConstants [Value_parameters]
AllocReturnsNull [Value_parameters]
AllocatedContextValid [Value_parameters]
Analysis [Gui_eval.S]
Analysis
ApronBox [Value_parameters]
ApronOctagon [Value_parameters]
ApronStorage [Value_parameters]
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.

ArrayPrecisionLevel [Value_parameters]
AutomaticContextMaxDepth [Value_parameters]
AutomaticContextMaxWidth [Value_parameters]
B
Backward_formals

Functions related to the backward propagation of the value of formals at the end of a call.

BaseToHCESet [Hcexprs]

Maps froms Base.t to set of HCE.t.

BitwiseOffsmDomain [Value_parameters]
BitwiseOffsmStorage [Value_parameters]
Box [Apron_domain]

Intervals abstract domain.

Builtins

Value analysis builtin shipped with Frama-C, more efficient than their equivalent in C

BuiltinsAuto [Value_parameters]
BuiltinsList [Value_parameters]
BuiltinsOverrides [Value_parameters]
Builtins_float

Builtins for standard floating-point functions.

Builtins_malloc

Dynamic allocation related builtins.

Builtins_misc

Builtins for normalization and dumping of values or state.

Builtins_nonfree

Non-free Value builtins.

Builtins_nonfree_print_c

Translate a Value state into a bunch of C assertions

Builtins_nonfree_watchpoint
Builtins_split
Builtins_string

Value builtins related to functions in string.h.

C
CVal [Main_values]

Abstract values built over Cvalue.V

Callsite [Value_types]
Callstack [Value_types]
CardinalEstimate [Cvalue]

Estimation of the cardinal of the concretization of an abstract state or value.

CilE

Value analysis alarms

Clear_Valuation [Eval]
Complete [Domain_builder]
Complete_Minimal [Domain_builder]
Complete_Minimal_with_datatype [Domain_builder]
Complete_Simple_Cvalue [Domain_builder]
Compute_functions

Value analysis of entire functions, using Eva engine.

Computer [Partitioned_dataflow]
Cvalue

Representation of Value's abstract memory.

CvalueDomain [Value_parameters]
CvalueOffsm [Offsm_value]
Cvalue_backward

Abstract reductions on Cvalue.V.t

Cvalue_domain

Main domain of the Value Analysis.

Cvalue_forward

Forward operations on Cvalue.V.t

Cvalue_init

Creation of the initial state for Value

Cvalue_specification

No function exported.

Cvalue_transfer

Transfer functions for the main domain of the Value analysis.

D
D [Inout_domain]
D [Symbolic_locs]
D [Offsm_domain]
D [Gauges_domain]
DatatypeIntegerRange [Eval_typ]
Default [Abstractions]
Default_offsetmap [Cvalue]

Values bound by default to a variable.

DegenerationPoints [Value_util]
Dom [Abstractions.S]
Domain_builder

Automatic builders to complete abstract domains from different simplified interfaces.

Domain_lift
Domain_product
Domain_store
E
E [Hcexprs]
EnumerateCond [Value_parameters]
Equality

Representation of an equality between a set of elements.

Equality

Equalities between syntactic lvalues and expressions.

EqualityCall [Value_parameters]
EqualityCallFunction [Value_parameters]
EqualityDomain [Value_parameters]
EqualityStorage [Value_parameters]
Equality_domain

Initial abstract state at the beginning of a call.

Eval
Eval_annots
Eval_op

Numeric evaluation.

Eval_terms

Evaluation of terms and predicates

Eval_typ
Evaluation
F
Flagged_Value [Eval]
ForceValues [Value_parameters]
Function_args

Nothing is exported; the function compute_atual is registered in Db.Value.

G
GCallstackMap [Gui_types]
GaugesDomain [Value_parameters]
GaugesStorage [Value_parameters]
Gauges_domain

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

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
H
HCE [Hcexprs]

Datatype + utilities functions for hashconsed exprsessions.

HCESet [Hcexprs]

Hashconsed sets of symbolic expressions.

HCEToZone [Hcexprs]

Maps from symbolic expressions to their memory dependencies, expressed as a Locations.Zone.t.

Hashtbl [Datatype.S_with_collections]
Hcexprs

Hash-consed expressions and lvalues.

I
IgnoreRecursiveCalls [Value_parameters]
Initialization

Creation of the initial state of abstract domain.

InitializationPaddingGlobals [Value_parameters]
InitializedLocals [Value_parameters]
InoutDomain [Value_parameters]
Inout_domain

Computation of inputs of outputs.

InterpreterMode [Value_parameters]
Interval [Main_values]

Dummy interval: no forward nor backward propagations.

J
JoinResults [Value_parameters]
K
Key [Datatype.Hashtbl]

Datatype for the keys of the hashtbl.

Key [Datatype.Map]

Datatype for the keys of the map.

Key_Domain [Structure]

Keys module for the abstract domains of Eva.

Key_Location [Structure]

Keys module for the abstract locations of Eva.

Key_Value [Structure]

Keys module for the abstract values of Eva.

L
Legacy [Abstractions]
Library_functions
LinearLevel [Value_parameters]
LoadFunctionState [Value_parameters]
Loc [Abstractions.S]
Locals_scoping

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

Location_lift
M
Main_locations

Main memory locations of Eva:

Main_values

Main numeric values of Eva.

Make [Gui_eval]
Make [Gui_types]

The types below depend on the abstract values currently available.

Make [Analysis]
Make [Compute_functions]
Make [Initialization]
Make [Mem_exec]
Make [Partitioning]

Partition of the abstract states, computed for each node by the dataflow analysis.

Make [Transfer_specification]
Make [Transfer_stmt]
Make [Evaluation]

Generic functor.

Make [Subdivided_evaluation]
Make [Transfer_logic]
Make [Powerset]

Set of states, propagated through the edges by the dataflow analysis.

Make [Datatype.Hashtbl]

Build a datatype of the hashtbl according to the datatype of values in the hashtbl.

Make [Datatype.Map]

Build a datatype of the map according to the datatype of values in the map.

Make [Equality_domain]
Make [Unit_domain]
Make [Domain_lift]
Make [Domain_product]
Make [Domain_store]
Make [Location_lift]
Make [Value_product]
Make [Structure]
Make_Domain [Simple_memory]
Make_Memory [Simple_memory]
MallocFunctions [Value_parameters]
MallocLevel [Value_parameters]
Map [Datatype.S_with_collections]
Mark_noresults
MemExecAll [Value_parameters]
Mem_exec
MemoryFootprint [Value_parameters]
Model [Cvalue]

Memories.

N
NoResultsAll [Value_parameters]
NoResultsFunctions [Value_parameters]
O
ObviouslyTerminatesAll [Value_parameters]
ObviouslyTerminatesFunctions [Value_parameters]
Octagon [Apron_domain]

Octagons abstract domain.

Offsm [Offsm_value]
Offsm_domain
Offsm_value
Open [Structure]

Opens an internal tree module into an external one.

OracleDepth [Value_parameters]
P
PLoc [Main_locations]

Abstract locations built over Precise_locs.

Partitioned_dataflow
Partitioning
Per_stmt_slevel

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

PolkaEqualities [Value_parameters]
PolkaLoose [Value_parameters]
PolkaStrict [Value_parameters]
Polka_Equalities [Apron_domain]

Linear equalities.

Polka_Loose [Apron_domain]

Loose polyhedra of the NewPolka library.

Polka_Strict [Apron_domain]

Strict polyhedra of the NewPolka library.

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

PrintCallstacks [Value_parameters]
PrinterDomain [Value_parameters]
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.

R
Recursion

Handling of recursion cycles in the callgraph

Red_statuses
ReduceOnLogicAlarms [Value_parameters]
ReductionDepth [Value_parameters]
Register

Functions of the Value plugin registered in Db.

Register_gui

Extension of the GUI in order to support the value analysis.

ResultsCallstack [Value_parameters]
RmAssert [Value_parameters]
S
SaveFunctionState [Value_parameters]
SemanticUnrollingLevel [Value_parameters]
Set [Datatype.S_with_collections]
Set [Equality]

Sets of equalities.

ShowSlevel [Value_parameters]
SignDomain [Value_parameters]
Sign_domain

Abstraction of the sign of integer variables.

Sign_value

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

Simple_memory

Simple memory abstraction for scalar non-volatile variables, built upon a value abstraction.

Simpler_domains

Simplified interfaces for abstract domains.

SkipLibcSpecs [Value_parameters]
SlevelFunction [Value_parameters]
SlevelMergeAfterLoop [Value_parameters]
SplitGlobalStrategy [Value_parameters]
SplitReturnFunction [Value_parameters]
Split_return

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

Split_strategy
State [Cvalue_domain]
State_import

Saving/loading of Value states, possibly among different ASTs.

Status [Alarmset]
StopAtNthAlarm [Value_parameters]
Store [Abstract_domain.Internal]
String_alarms [Builtins_string]

Alarms are pairs (assertion, warning_msg): ACSL "assertion", Informative message on why the evaluation raised an alarm

Structure

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

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.

Subpart [Cvalue_domain]
SymbolicLocsDomain [Value_parameters]
SymbolicLocsStorage [Value_parameters]
Symbolic_locs

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

T
Transfer [Abstract_domain.S]

Transfer functions from the result of evaluations.

Transfer [Cvalue_transfer]
Transfer_logic
Transfer_specification
Transfer_stmt
U
UndefinedPointerComparisonPropagateAll [Value_parameters]
Unit_domain
UsePrototype [Value_parameters]
V
V [Cvalue]

Values.

V_Offsetmap [Cvalue]

Memory slices.

V_Or_Uninitialized [Cvalue]

Values with 'undefined' and 'escaping addresses' flags.

Val [Abstractions.S]
ValPerfFlamegraphs [Value_parameters]
ValShowInitialState [Value_parameters]
ValShowPerf [Value_parameters]
ValShowProgress [Value_parameters]
Valuation [Evaluation.S]

Results of an evaluation: the results of all intermediate calculation (the value of each expression and the location of each lvalue) are cached here.

Value

Analysis for values and pointers

Value_parameters
Value_perf

Call start_doing when starting analyzing a new function.

Value_product

Cartesian product of two value abstractions.

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_results [Value]
Value_types

Declarations that are useful for plugins written on top of the results of Value.

Value_util
W
Warn

Alarms and imprecision warnings emitted during the analysis.

WarnBuiltinOverride [Value_parameters]
WarnCopyIndeterminate [Value_parameters]
WarnLeftShiftNegative [Value_parameters]
WarnPointerComparison [Value_parameters]
WarnPointerSubstraction [Value_parameters]
WarnSignedConvertedDowncast [Value_parameters]
Widen

Per-function computation of widening hints.

Widen_hints_ext

Syntax extension for widening hints, used by Value.

Widen_type

Widening hints for the Value Analysis datastructures.

WideningLevel [Value_parameters]