Index of modules


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]