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 [Eval_annots]
Alarm_cache [Value_messages]
Alarm_key [Value_messages]
Alarmset
Map from alarms to status.
AllRoundingModes [Value_parameters]
AllRoundingModesConstants [Value_parameters]
AllocatedContextValid [Value_parameters]
ApronBox [Value_parameters]
ApronOctagon [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]
Atom [Equality_term]
AutomaticContextMaxDepth [Value_parameters]
AutomaticContextMaxWidth [Value_parameters]

B
BitwiseOffsmDomain [Value_parameters]
Box [Apron_domain]
Intervals abstract domain.
Builtins
Value analysis builtin shipped with Frama-C, more efficient than their equivalent in C
BuiltinsOverrides [Value_parameters]
Builtins_float
Builtins for standard floating-point functions.
Builtins_nonfree
Non-free Value builtins.
Builtins_nonfree_deterministic
Non-free Value builtins for deterministic code.
Builtins_nonfree_malloc
Dynamic allocation related builtins.
Builtins_nonfree_print_c
Translate a Value state into a bunch of C assertions
Builtins_nonfree_string
Non-free Value builtins.
Builtins_nonfree_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]
Compute_functions
Value analysis of entire functions, using Eva engine.
Computer [Partitioned_dataflow]
Computer [Eval_slevel]
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_transfer
Transfer functions for the main domain of the Value analysis.

D
D [Offsm_domain]
Default [Abstractions]
Default_offsetmap [Cvalue]
Values bound by default to a variable.
DegenerationPoints [Value_util]
Dom [Abstractions.S]
Domain_lift
Domain_product

E
EnumerateCond [Value_parameters]
Equality
Type of the keys of the map.
EqualityDomain [Value_parameters]
Equality_domain
Equality_sig
Signature for Equality module, that implements equalities over ordered types
Equality_term
Atom of the predicates.
Eva [Value_parameters]
Eval
Types and functions related to evaluations.
Eval_annots
Check the postcondition of kf for a given behavior b.
Eval_behaviors
Evaluation of functions using their specification
Eval_exprs
Reduction by operators condition
Eval_funs
Value analysis of entire functions, using the legacy engine.
Eval_non_linear
Evaluation of non-linear expressions.
Eval_op
Numeric evaluation.
Eval_slevel
Value analysis of statements and functions bodies with slevel.
Eval_stmt
Value analysis of statements and functions bodies.
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
FloatTimingStep [Value_parameters]
ForceValues [Value_parameters]
Function_args

G
GCallstackMap [Gui_types]
Gui_callstacks_filters
Filtering on analysis callstacks
Gui_eval
This module defines an abstraction to evaluate various things across multiple callstacks.
Gui_types

H
HashBehaviors [Eval_annots.ActiveBehaviors]
Hashtbl [Datatype.S_with_collections]
Hptset [Equality_term.Atom]

I
IgnoreRecursiveCalls [Value_parameters]
Initial_state
Creation of the initial state for Value.
Initialization
Creation of the inital 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
LOffset [Lmap_bitwise.Location_map_bitwise]
Lattice_Set [Equality_term.Atom]
Legacy [Abstractions]
Library_functions
Fake varinfo used by Value to store the result of functions without bodies.
LinearLevel [Value_parameters]
Lmap_Bitwise [Equality_term.Atom]
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 [Initialization]
Make [Mem_exec2]
Make [Transfer_stmt]
Make [Transfer_logic]
Make [Non_linear_evaluation]
Make [Evaluation]
Generic functor.
Make [Equality_domain]
Make [Equality]
Make [Unit_domain]
Make [Domain_lift]
Make [Domain_product]
Make [Location_lift]
Make [Value_product]
Make [Structure]
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_Partition [Partitioning]
Partition of the abstract states, computed for each node by the dataflow analysis.
Make_Set [Partitioning]
Set of states, propagated through the edges by the dataflow analysis.
Map [Datatype.S_with_collections]
Mark_noresults
MemExecAll [Value_parameters]
Mem_exec
This module memorizes the analysis of entire calls to a function, so that those analyzes can be reused later on.
Mem_exec2
Counter that must be used each time a new call is analyzed, in order to refer to it later
Mem_lvalue
Improved handling of l-values that are read/written multiple times in a function.
MemoryFootprint [Value_parameters]
Model [Cvalue]
Memories.

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

O
O [Lattice_type.Lattice_Hashconsed_Set]
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
Set of states, propagated through the edges 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.
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
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]
ReusedExprs [Value_parameters]
RmAssert [Value_parameters]

S
SaveFunctionState [Value_parameters]
SemanticUnrollingLevel [Value_parameters]
Separate
SeparateStmtOf [Value_parameters]
SeparateStmtStart [Value_parameters]
SeparateStmtWord [Value_parameters]
Set [Equality_sig.S_with_collections]
Set [Datatype.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_imp
Sets of Cvalue.Model.t implemented imperatively.
State_import
Saving/loading of Value states, possibly among different ASTs.
State_set
Functional sets of Cvalue.Model.t, currently implemented as lists without repetition.
Status [Alarmset]
StopAtNthAlarm [Value_parameters]
Stop_at_nth
Structure
Gadt describing the structure of a tree of different data types, and providing fast accessors of its nodes.
Subpart [Cvalue_domain]
Summary [Abstract_domain.S]
Datatypes
Summary [Mem_exec2.Domain]

T
Transfer [Abstract_domain.S]
Transfer functions from the result of evaluations.
Transfer [Cvalue_transfer]
Transfer_logic
Check the postcondition of kf for a given behavior b.
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]
ValShowInitialState [Value_parameters]
ValShowPerf [Value_parameters]
ValShowProgress [Value_parameters]
Valarms
Emission of alarms.
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
ValueOutputs [Mem_exec]
Subtype of Value_types.call_res
Value_Message_Callback [Value_messages]
Value_messages
UNDOCUMENTED.
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
Callstacks related types and functions

W
Warn
Alarms and imprecision warnings emitted during the analysis.
WarnCopyIndeterminate [Value_parameters]
WarnLeftShiftNegative [Value_parameters]
WarnPointerComparison [Value_parameters]
WarnPointerSubstraction [Value_parameters]
Widen
Per-function computation of widening hints.
Widen_type
Widening hints for the Value Analysis datastructures.
WideningLevel [Value_parameters]