Index of modules


A
ActiveBehaviors [Eval_annots]
Actuals [Mem_exec]
ActualsList [Mem_exec]
AllRoundingModes [Value_parameters]
AllRoundingModesConstants [Value_parameters]
AllocatedContextValid [Value_parameters]
ArrayPrecisionLevel [Value_parameters]
AutoStrategy [Split_return]
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_nonfree
Non-free Value builtins.
Builtins_nonfree_deterministic
Non-free Value builtins for deterministic code.
Builtins_nonfree_malloc
Builtin for free function
Builtins_nonfree_print_c
Translate a Value state into a bunch of C assertions
Builtins_nonfree_watchpoint

C
Call_info [Value_perf]
Call_site [Value_perf]
Callers [Kf_state]
Computer [Eval_slevel]
ContextfreeGlobals [Initial_state]
Current_table
Internal state of the Value Analysis during analysis.

D
DatatypeSlevel [Per_stmt_slevel]
DegeneratedHighlighted [Register_gui]
DegenerationPoints [Value_util]
Dfs [Per_stmt_slevel]
DumpFileCounters [Builtins]
Dynamic_Alloc_Bases [Builtins_nonfree_malloc]
Dynamic_Alloc_Infinite_Table [Builtins_nonfree_malloc]

E
Eval_annots
Statuses for code annotations and function contracts
Eval_exprs
Detects if an expression can be considered as a lvalue even though it is hidden by a cast that does not change the lvalue.
Eval_funs
Value analysis of entire functions
Eval_op
Numeric evaluation.
Eval_slevel
Value analysis of statements and functions bodies
Eval_stmt
Value analysis of statements and functions bodies
Eval_terms
Truth values for a predicate analyzed by the value analysis

F
Fc_config [Value_parameters]
FloatTimingStep [Value_parameters]
ForKf [Per_stmt_slevel]
ForceValues [Value_parameters]
Function_args

G
G [Per_stmt_slevel]
Got_Imprecise_Value [Value_util]

H
HashBehaviors [Eval_annots.ActiveBehaviors]
Hashtbl [Datatype.S_with_collections]
Hashtbl [Value_perf.Imperative_callstack_trie]
Hints [Widen]
Hptset [Cil_datatype.Stmt]

I
ILevel [Value_parameters]
IgnoreRecursiveCalls [Value_parameters]
Imperative_callstack_trie [Value_perf]
InitialStateChanged [Value_parameters]
Initial_state
Creation of the initial state for Value
InitializedPaddingGlobals [Value_parameters]
InterpreterMode [Value_parameters]
Is_Called [Kf_state]

K
Key [Datatype.Hashtbl]
Datatype for the keys of the hashtbl.
Key [Datatype.Map]
Datatype for the keys of the map.
KfStrategy [Split_return]
Kf_state
Is called
Ki [Non_linear]

L
LeftShiftNegativeOld [Value_parameters]
Library_functions
Associates kernel_function to a fresh base for the address returned by the kernel_function.
Loc_hashtbl [Non_linear]
LocalSlevelAnnots [Per_stmt_slevel]
LocalSlevelId [Per_stmt_slevel]
Locals_scoping
Auxiliary functions to mark invalid (more precisely 'escaping') the references to a variable whose scope ends.
Location_list [Non_linear]

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.
MallocFunctions [Builtins_nonfree_malloc]
MallocPrecision [Builtins_nonfree_malloc]
MallocedByStack [Builtins_nonfree_malloc]
Map [Datatype.S_with_collections]
MapActualsBasesInputsPrevious [Mem_exec]
MapBasesInputsPrevious [Mem_exec]
MapInputsPrevious [Mem_exec]
MapLval [Split_return.ReturnUsage]
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.
MemoryFootprint [Value_parameters]

N
NoResultsAll [Value_parameters]
NoResultsFunctions [Value_parameters]
Non_linear
Non_linear_assignments [Non_linear]

O
ObviouslyTerminatesAll [Value_parameters]
ObviouslyTerminatesFunctions [Value_parameters]

P
Per_stmt_slevel
Same slevel i in the entire function
Perf_by_callstack [Value_perf]
Precise_locs
This module provide 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.
PreviousState [Mem_exec]
PreviousStates [Mem_exec]
PrintCallstacks [Value_parameters]

R
RUDatatype [Split_return.ReturnUsage]
RankedMallocedByStack [Builtins_nonfree_malloc]
Register
Function of the value plugin registered in the kernel
Register_gui
Extension of the GUI in order to support the value analysis.
ResultFromCallback [Mem_exec]
ResultsAfter [Value_parameters]
ResultsCallstack [Value_parameters]
Retres [Library_functions]
ReturnUsage [Split_return]
Returned_Val [Library_functions]
Associates kernel_function to a fresh base for the address returned by the kernel_function.
RmAssert [Value_parameters]

S
SaveCounter [Mem_exec]
SemanticUnrollingLevel [Value_parameters]
Separate
SeparateStmtOf [Value_parameters]
SeparateStmtStart [Value_parameters]
SeparateStmtWord [Value_parameters]
Set [Datatype.S_with_collections]
ShowSlevel [Value_parameters]
ShowTrace [Value_parameters]
Sindexed [State_imp]
SlevelFunction [Value_parameters]
SlevelMergeAfterLoop [Value_parameters]
SplitReturnAuto [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.
StmtStartData [Eval_slevel.Computer]
StopAtNthAlarm [Value_parameters]
Stop_at_nth
Subdivide_float_in_expr [Value_parameters]

T
Terminating_calls [Value_results]
TimingStep [Value_parameters]

U
UndefinedPointerComparisonPropagateAll [Value_parameters]
UsePrototype [Value_parameters]
UsedVarState [Register_gui]

V
V [Per_stmt_slevel.G]
ValShowInitialState [Value_parameters]
ValShowPerf [Value_parameters]
ValShowProgress [Value_parameters]
ValueOutputs [Mem_exec]
Subtype of Value_types.call_res
Value_parameters
Value_perf
Call start_doing when starting analyzing a new function.
Value_results
Value_util
Callstacks related types and functions

W
Warn
Check that kf is not already present in the call stack
WarnCopyIndeterminate [Value_parameters]
WarnLeftShiftNegative [Value_parameters]
WarnPointerSubstraction [Value_parameters]
Widen
WideningLevel [Value_parameters]