Index of modules


A
Abs_Err [Numerors_arithmetics]
Abstract
Internal and External signature of abstractions used in the Eva engine.
Abstract_domain
Abstract domains of the analysis.
Abstract_location
Abstract memory locations of the analysis.
Abstract_value
Abstract numeric values of the analysis.
Abstractions
Registration and building of the analysis abstractions.
ActiveBehaviors [Transfer_logic]
AlarmOrProp [Red_statuses]
AlarmsWarnings [Value_parameters]
Alarmset
Map from alarms to status.
AllRoundingModesConstants [Value_parameters]
AllocFunctions [Value_parameters]
AllocReturnsNull [Value_parameters]
AllocatedContextValid [Value_parameters]
Analysis [Gui_eval.S]
Analysis
The abstractions used in the latest analysis, and its results.
Approx [Numerors_arithmetics]
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]
AutoLoopUnroll [Value_parameters]
Auto_loop_unroll
Heuristic for automatic loop unrolling.
AutomaticContextMaxDepth [Value_parameters]
AutomaticContextMaxWidth [Value_parameters]

B
Backward [Numerors_arithmetics.Arithmetic]
Backward_Comparisons [Numerors_arithmetics]
Backward comparisons
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.
BitwiseOffsmStorage [Value_parameters]
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_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

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 [Iterator]
Config [Abstractions]
Configuration defining the abstractions to be used in an analysis.
Cvalue
Representation of Value's abstract memory.
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_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.

D
D [Inout_domain]
D [Symbolic_locs]
D [Offsm_domain]
D [Gauges_domain]
D [Traces_domain]
DatatypeIntegerRange [Eval_typ]
Default [Abstractions]
DefaultLoopUnroll [Value_parameters]
Default_offsetmap [Cvalue]
Values bound by default to a variable.
DegenerationPoints [Value_util]
DescendingIteration [Value_parameters]
Dom [Abstractions.S]
Domain [Abstract]
Key and structure for abstract domains.
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
Domains [Value_parameters]
DomainsFunction [Value_parameters]

E
E [Hcexprs]
Edge [Traces_domain]
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]
EqualityStorage [Value_parameters]
Equality_domain
Initial abstract state at the beginning of a call.
Eva
Analysis for values and pointers
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 [Abstractions.Eva]
Eval
Types and functions related to evaluations.
Eval_annots
Eval_op
Numeric evaluation.
Eval_terms
Evaluation of terms and predicates
Eval_terms [Eva]
Eval_typ
Functions related to type conversions
Evaluation
Generic evaluation and reduction of expressions and left values.
Exact [Numerors_arithmetics]
Modules which implement the previous signature for each field of <t>

F
Flagged_Value [Eval]
ForceValues [Value_parameters]
Forward [Numerors_arithmetics.Arithmetic]
Function_Mode [Domain_mode]
Function_args
Nothing is exported; the function compute_atual is registered in Db.Value.

G
GCallstackMap [Gui_types]
GaugesStorage [Value_parameters]
Gauges_domain
Gauges domain ("Arnaud Venet: The Gauge Domain: Scalable Analysis of Linear Inequality Invariants.
Graph [Traces_domain]
GraphShape [Traces_domain]
Can't use Graph.t it needs an impossible recursive module
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.

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.
HierarchicalConvergence [Value_parameters]
HistoryPartitioning [Value_parameters]

I
I [Numerors_arithmetics]
IgnoreRecursiveCalls [Value_parameters]
Initialization
Creation of the initial state of abstract domain.
InitializationPaddingGlobals [Value_parameters]
InitializedLocals [Value_parameters]
Inout_domain
Computation of inputs of outputs.
InterpreterMode [Value_parameters]
Interval [Main_values]
Dummy interval: no forward nor backward propagations.
Iterator
Mark the analysis as aborted.

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 [Partition]
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
Fake varinfo used by Value to store the result of functions.
LinearLevel [Value_parameters]
LinearLevelFunction [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 [Abstract]
Key and structure for abstract locations.
Location_lift
Loops [Traces_domain]

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 [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 [Analysis]
Make [Compute_functions]
Make [Initialization]
Make [Mem_exec]
Make [Trace_partitioning]
Make [Partitioning_index]
Partition of the abstract states, computed for each node by the dataflow analysis.
Make [Partitioning_parameters]
Make [Auto_loop_unroll]
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 [Equality_domain]
Make [Unit_domain]
Make [Domain_lift]
Make [Domain_product]
Make [Domain_store]
Make [Location_lift]
Make [Value_product]
Make [Structure]
MakeFlow [Partition]
Flows are used to transfer states from one partition to another, by applying transfer functions and partitioning actions.
Make_Domain [Simple_memory]
Make_Memory [Simple_memory]
MallocLevel [Value_parameters]
Map [Datatype.S_with_collections]
Mark_noresults
MemExecAll [Value_parameters]
Mem_exec
Counter that must be used each time a new call is analyzed, in order to refer to it later
MinLoopUnroll [Value_parameters]
Mode [Numerors_utils]
Mode [Domain_mode]
Datatype for modes.
Model [Cvalue]
Memories.

N
NoResultsFunctions [Value_parameters]
Node [Traces_domain]
NumerorsLogFile [Value_parameters]
Numerors_Mode [Value_parameters]
Numerors_Real_Size [Value_parameters]
Numerors_arithmetics
Type manipulated by the arithmetics
Numerors_domain
Numerors domain: computes over-approximations of the rounding errors bounds of floating-point computations.
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.

O
OctagonCall [Value_parameters]
Octagons
Offsm [Offsm_value]
Offsm_domain
If true, the offsetmap domain stores information that can probably be re-synthesized from the value domain.
Offsm_value
Auxiliary functions
Open [Structure]
Opens an internal tree module into an external one.
OracleDepth [Value_parameters]

P
PLoc [Main_locations]
Abstract locations built over Precise_locs.
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.
Powerset
Set of states, propagated through the edges by the dataflow analysis.
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.
Precision [Value_parameters]
Meta-option
Precisions [Numerors_utils]
PrintCallstacks [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
This modules stores the alarms and properties for which a red status has been emitted.
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.
Rel_Err [Numerors_arithmetics]
ReportRedStatuses [Value_parameters]
Restrict [Domain_builder]
ResultsAll [Value_parameters]
RmAssert [Value_parameters]
Rounding [Numerors_utils]

S
SaveFunctionState [Value_parameters]
SemanticUnrollingLevel [Value_parameters]
Set [Datatype.S_with_collections]
Set [Equality]
Sets of equalities.
Shape [Structure]
ShowSlevel [Value_parameters]
Sign [Numerors_utils]
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]
SplitLimit [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]
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]
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
Trace_partitioning
The states being partitioned
TracesDot [Value_parameters]
TracesProject [Value_parameters]
TracesUnifyLoop [Value_parameters]
TracesUnrollLoop [Value_parameters]
Traces_domain
Traces domain
Transfer_logic
Check the postcondition of kf for the list of behaviors.
Transfer_specification
Transfer_stmt
Applies the show_each or dump_each directives.

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 [Abstract]
Key and structure for abstract values.
ValuePartitioning [Value_parameters]
Value_parameters
Dynamic allocation
Value_parameters [Eva]
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 [Eva]
Value_types
Declarations that are useful for plugins written on top of the results of Value.
Value_util
Callstacks related types and functions

W
Warn
Alarms and imprecision warnings emitted during the analysis.
WarnCopyIndeterminate [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.
WideningDelay [Value_parameters]
WideningPeriod [Value_parameters]