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]
AlarmsWarnings [Value_parameters]
Alarmset
Map from alarms to status.
AllRoundingModes [Value_parameters]
AllRoundingModesConstants [Value_parameters]
AllocatedContextValid [Value_parameters]
Analysis
The abstractions used in the latest analysis, and its results.
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_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]
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
Evaluation of functions using their specification
Cvalue_transfer
Transfer functions for the main domain of the Value analysis.

D
D [Symbolic_locs]
D [Offsm_domain]
D [Gauges_domain]
DatatypeIntegerRange [Eval_typ]
Datatype_UHCE [Hcexprs]
Default [Abstractions]
Default_offsetmap [Cvalue]
Values bound by default to a variable.
DegenerationPoints [Value_util]
Dom [Abstractions.S]
Domain_builder
Domain_lift
Domain_product
Domain_store

E
EnumerateCond [Value_parameters]
Equality
Type of the keys of the map.
EqualityDomain [Value_parameters]
EqualityStorage [Value_parameters]
Equality_domain
Initial abstract state at the beginning of a call.
Equality_sig
Signature for Equality module, that implements equalities over ordered types
Eval
Types and functions related to evaluations.
Eval_annots
Eval_op
Numeric evaluation.
Eval_terms
Evaluation of terms and predicates
Eval_typ
Functions related to type conversions
Evaluation
Generic evaluation and reduction of expressions and left values.

F
ForceValues [Value_parameters]
Function_args
Nothing is exported; the function compute_atual is registered in Db.Value.

G
GCallstackMap [Gui_types]
GaugesDomain [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_eval
This module defines an abstraction to evaluate various things across multiple callstacks.
Gui_types

H
HCE [Hcexprs]
Datatype + utilities functions for Hcexprs.hashconsed_exprs.
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]
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
Fake varinfo used by Value to store the result of 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 [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_stmt]
Make [Non_linear_evaluation]
Same functionalities as Eva.
Make [Evaluation]
Generic functor.
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 [Equality]
Make [Unit_domain]
Make [Domain_lift]
Make [Domain_product]
Make [Domain_store]
Make [Location_lift]
Make [Value_product]
Make [Structure]
MakeInternal [Equality_domain]
MallocFunctions [Value_parameters]
MallocLevel [Value_parameters]
MallocReturnsNull [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
MemoryFootprint [Value_parameters]
Model [Cvalue]
Memories.

N
NoResultsAll [Value_parameters]
NoResultsFunctions [Value_parameters]
Non_linear_evaluation
Evaluation of non-linear expressions.

O
ObviouslyTerminatesAll [Value_parameters]
ObviouslyTerminatesFunctions [Value_parameters]
Octagon [Apron_domain]
Octagons abstract domain.
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.
Partitioned_dataflow
Mark the analysis as aborted.
Partitioning
Partition of the abstract states, computed for each node by the dataflow analysis.
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
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.
PrintCallstacks [Value_parameters]

R
Recursion
Handling of recursion cycles in the callgraph
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]
Separate
SeparateStmtOf [Value_parameters]
SeparateStmtStart [Value_parameters]
SeparateStmtWord [Value_parameters]
Set [Datatype.S_with_collections]
Set [Equality_sig.S_with_collections]
ShowSlevel [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]
Stop_at_nth
Store [Transfer_stmt.Domain]
Store [Abstract_domain.Internal]
String_alarms [Builtins_string]
Alarms are triples (kind, text, warning_msg): Alarm kind, Message text (to be emitted via emit_alarm), Warning message (to be emitted via Value_util.alarm_report)
Structure
Gadt describing the structure of a tree of different data types, and providing fast accessors of its nodes.
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
Check the postcondition of kf for the list of behaviors.
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
Dynamic allocation
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
Callstacks related types and functions

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]