A | |
ActiveBehaviors [Eval_annots] | |
Alarm_cache [Value_messages] | |
Alarm_key [Value_messages] | |
AllRoundingModes [Value_parameters] | |
AllRoundingModesConstants [Value_parameters] | |
AllocatedContextValid [Value_parameters] | |
ArrayPrecisionLevel [Value_parameters] | |
AutomaticContextMaxDepth [Value_parameters] | |
AutomaticContextMaxWidth [Value_parameters] | |
B | |
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_watchpoint | |
C | |
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
|
Compute [Mem_lvalue] | |
Computer [Eval_slevel] | |
Cvalue |
Representation of Value's abstract memory.
|
D | |
Default_offsetmap [Cvalue] |
Values bound by default to a variable.
|
DegenerationPoints [Value_util] | |
Dynamic_Alloc_Bases [Builtins_nonfree_malloc] | |
E | |
Eval_annots |
Statuses for code annotations and function contracts
|
Eval_exprs |
Reduction by operators condition
|
Eval_funs |
Value analysis of entire functions.
|
Eval_non_linear |
Evaluation of non-linear expressions.
|
Eval_op |
Numeric evaluation.
|
Eval_slevel |
Mark the analysis as aborted.
|
Eval_stmt |
Value analysis of statements and functions bodies
|
Eval_terms |
Evaluation of terms and predicates
|
Eval_typ |
This module contains functions related to type conversions
|
F | |
FloatTimingStep [Value_parameters] | |
ForceValues [Value_parameters] | |
Function_args |
For all formals of
kf whose address is taken, merge their values
in prev_state and new_state , and update new_state .
|
G | |
GCallstackMap [Gui_types] | |
GraphDeps [Mem_lvalue] | |
Gui_callstacks_filters |
Filtering on analysis callstacks
|
Gui_eval |
This module defines an abstraction to evaluate various things across
multiple callstacks.
|
Gui_types | |
H | |
HLV [Mem_lvalue] | |
HashBehaviors [Eval_annots.ActiveBehaviors] | |
Hashtbl [Datatype.S_with_collections] | |
I | |
IgnoreRecursiveCalls [Value_parameters] | |
Initial_state |
Creation of the initial state for Value
|
InitializationPaddingGlobals [Value_parameters] | |
InterpreterMode [Value_parameters] | |
J | |
JoinResults [Value_parameters] | |
K | |
KernelFile [Mem_lvalue] | |
Key [Datatype.Hashtbl] |
Datatype for the keys of the hashtbl.
|
Key [Datatype.Map] |
Datatype for the keys of the map.
|
L | |
LatticeDirty [Mem_lvalue] | |
Library_functions |
Associates
kernel_function to a fresh base for the address returned by
the kernel_function .
|
LinearLevel [Value_parameters] | |
Locals_scoping |
Auxiliary functions to mark invalid (more precisely 'escaping') the
references to a variable whose scope ends.
|
M | |
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.
|
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_lvalue |
Does the evaluation of
stmt modifies the eventual value of X.lv ?
|
MemoryFootprint [Value_parameters] | |
Model [Cvalue] |
Memories.
|
N | |
NoResultsAll [Value_parameters] | |
NoResultsFunctions [Value_parameters] | |
O | |
ObviouslyTerminatesAll [Value_parameters] | |
ObviouslyTerminatesFunctions [Value_parameters] | |
P | |
Per_stmt_slevel |
Fine-tuning for slevel, according to
//@ slevel directives.
|
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 | |
Register |
Function of the value plugin registered in the kernel
|
Register_gui |
Extension of the GUI in order to support the value analysis.
|
ResultsCallstack [Value_parameters] | |
ReusedExprs [Value_parameters] | |
RmAssert [Value_parameters] | |
S | |
SemanticUnrollingLevel [Value_parameters] | |
Separate | |
SeparateStmtOf [Value_parameters] | |
SeparateStmtStart [Value_parameters] | |
SeparateStmtWord [Value_parameters] | |
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_imp |
Sets of Cvalue.Model.t implemented imperatively.
|
State_set |
Functional sets of
Cvalue.Model.t , currently implemented as lists
without repetition.
|
StopAtNthAlarm [Value_parameters] | |
Stop_at_nth | |
T | |
TopologicalBefore [Mem_lvalue] | |
U | |
UndefinedPointerComparisonPropagateAll [Value_parameters] | |
UsePrototype [Value_parameters] | |
V | |
V [Cvalue] |
Values.
|
V [Mem_lvalue.GraphDeps] | |
V_Offsetmap [Cvalue] |
Memory slices.
|
V_Or_Uninitialized [Cvalue] |
Values with 'undefined' and 'escaping addresses' flags.
|
ValShowInitialState [Value_parameters] | |
ValShowPerf [Value_parameters] | |
ValShowProgress [Value_parameters] | |
Valarms |
division.
|
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_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_types |
Declarations that are useful for plugins written on top of the results
of Value.
|
Value_util |
A call_stack is a list, telling which function was called at which
site.
|
W | |
Warn |
This function should be used to treat a call
lv = kf(...) .
|
WarnCopyIndeterminate [Value_parameters] | |
WarnLeftShiftNegative [Value_parameters] | |
WarnPointerSubstraction [Value_parameters] | |
Widen | |
Widen_type |
Widening hints for the Value Analysis datastructures.
|
WideningLevel [Value_parameters] |