A | |
AbsoluteValidRange [Kernel] |
Behavior of option "-absolute-valid-range"
|
Abstract [Type] |
Apply this functor to access to the abstract type of the given name.
|
Abstract_interp |
Functors for generic lattices implementations.
|
Action [Parameter_sig.Builder] | |
AfterTable_By_Callstack [Db.Value] |
Table containing the state of the value analysis after the evaluation
of each reachable and evaluable statement.
|
AggressiveMerging [Kernel] |
Behavior of option "-aggressive-merging"
|
Alarms |
Alarms Database.
|
Allocates |
Generation of default
allocates \nothing clauses.
|
AllowDuplication [Kernel] |
Behavior of option "-allow-duplication".
|
Alpha |
Alpha conversion.
|
Analyses_manager |
Nothing exported.
|
Annotations |
Annotations in the AST.
|
Arity_One [Binary_cache] | |
Arity_Three [Binary_cache] | |
Arity_Two [Binary_cache] | |
Array [State_builder] | |
Array [Datatype] | |
Array_with_collections [Datatype] | |
As_string [Parameter_sig.Collection] |
A collection is a standard string parameter
|
AsmContractsAutoValidate [Kernel] |
Behavior of option "-asm-contracts-auto-validate."
|
AsmContractsGenerate [Kernel] |
Behavior of option "-asm-contracts"
|
Asm_contracts |
Code transformation for inferring contracts from information given
in GNU's extended assembly syntax.
|
Ast |
Access to the CIL AST which must be used from Frama-C.
|
Ast_info |
AST manipulation utilities.
|
Attribute [Cil_datatype] | |
Attributes [State_dependency_graph] | |
Attributes [Cil_datatype] | |
AutoLoadPlugins [Kernel] |
Behavior of option "-autoload-plugins"
|
B | |
Backwards [Dataflow2] | |
Backwards [Dataflow] | |
Bag |
List with constant-time concat operation.
|
Base | |
Base |
Abstraction of the base of an addressable memory zone, together with
the validity of the zone.
|
BigIntsHex [Kernel] |
Behavior of option "-hexadecimal-big-integers"
|
Binary_Predicate [Binary_cache] | |
Binary_cache |
Very low-level abstract functorial caches.
|
Binding [Journal] | |
Bit_utils |
Some bit manipulations.
|
Bitvector |
Bitvectors.
|
Block [Cil_datatype] | |
Bool [Parameter_sig.Builder] | |
Bool [Dynamic.Parameter] |
Boolean parameters.
|
Bool [Datatype] | |
Bool [Abstract_interp] | |
Bool_ref [State_builder] |
Build a reference on a boolean.
|
Bottom |
Types, monads and utilitary functions for lattices in which the bottom is
managed separately from other values.
|
Bound_Lattice [Bottom] |
Bounds a semi-lattice.
|
Build [Hook] |
Make a new empty hook from a given type of parameters.
|
Build_ordered [Hook] | |
Builtin_alarms [Fval] | |
Builtin_functions [Cil] |
A list of the built-in functions for the current compiler (GCC or
MSVC, depending on
!msvcMode ).
|
Builtin_logic_info [Cil_datatype] | |
Builtins [Logic_env] | |
C | |
C11 [Kernel] |
Behavior of option "-c11"
|
Cabs |
Untyped AST.
|
Cabs2cil |
Registers a new hook that will be applied each time a side-effect free
expression whose result is unused is dropped.
|
Cabs_debug | |
Cabs_file [Cil_datatype] | |
Cabshelper |
Helper functions for Cabs
|
Cabsvisit |
Variable or function prototype
name
|
Call_Type_Value_Callbacks [Db.Value] |
Actions to perform at each treatment of a "call"
statement.
|
Call_Value_Callbacks [Db.Value] |
Actions to perform at each treatment of a "call"
statement.
|
Callwise [Db.From] | |
Caml_weak_hashtbl [State_builder] |
Build a weak hashtbl over a datatype
Data by using Weak.Make provided
by the OCaml standard library.
|
Caml_weak_hashtbl [Datatype] | |
Category [Parameter_sig.Collection] |
Categories for this collection.
|
Category_set [Log] |
sets of category keywords
|
Cfg |
Code to compute the control-flow graph of a function or file.
|
Char [Transitioning] |
See above documentation for
String
|
Char [Datatype] | |
Check [Kernel] |
Behavior of option "-check"
|
Cil |
CIL main API.
|
Cil_const |
Smart constructors for some CIL data types
|
Cil_datatype |
Datatypes of some useful CIL types.
|
Cil_descriptive_printer |
Internal printer for Cabs2cil.
|
Cil_printer |
Internal Cil printer.
|
Cil_state_builder |
Functors for building computations which use kernel datatypes.
|
Cil_types |
The Abstract Syntax of CIL.
|
Cil_types_debug | |
Cilconfig |
Reading and storing configuration files from the filesystem.
|
Clexer |
The C Lexer.
|
Clone |
Experimental module
|
Cmdline |
Command line parsing.
|
CodeOutput [Kernel] |
Behavior of option "-ocode".
|
Code_annotation [Cil_datatype] | |
Command |
Useful high-level system operations.
|
Comments [Cabshelper] | |
Comp [Abstract_interp] |
Signatures for comparison operators
==, !=, <, >, <=, >= .
|
Comp_unused [Hptmap] |
Default implementation for the
Compositional_bool argument of the functor
Hptmap.Make .
|
Compinfo [Cil_datatype] | |
Compute_Statement_Callbacks [Db.Value] |
Actions to perform whenever a statement is handled.
|
Config [Plugin.S] |
Handle the specific `config' directory of the plug-in.
|
Config |
Information about version of Frama-C.
|
Config_dir [Kernel] |
Directory in which config files are searched.
|
Configuration [Gtk_helper] |
Configuration module for the GUI: all magic visual constants should
use this mechanism (window width, ratios, ...).
|
Consolidation [Property_status] |
Consolidation of a property status according to the (consolidated) status of
the hypotheses of the property.
|
Consolidation_graph [Property_status] |
See the consolidated status of a property in a graph, which all its
dependencies and their consolidated status.
|
ConstReadonly [Kernel] |
Global variables with
"const" qualifier are constant.
|
Constant [Cil_datatype] | |
Constant_Propagation [Db] |
Constant propagation plugin.
|
Constfold [Kernel] |
Behavior of option "-constfold"
|
ContinueOnAnnotError [Kernel] |
Behavior of option "-continue-annot-error"
|
Copy [Kernel] |
Behavior of option "-copy"
|
Counter [State_builder] |
Creates a projectified counter.
|
Cparser | |
CppCommand [Kernel] |
Behavior of option "-cpp-command"
|
CppExtraArgs [Kernel] |
Behavior of option "-cpp-extra-args"
|
CppGnuLike [Kernel] |
Behavior of option "-cpp-frama-c-compliant"
|
Cprint |
Printers for the Cabs AST
|
CurrentLoc [Cil_const] |
forward reference to current location (see
Cil.CurrentLoc )
|
CurrentLoc [Cil] |
A reference to the current location.
|
CustomAnnot [Kernel] |
Behavior of option "-custom-annot-char".
|
D | |
Dataflow |
Deprecated: use
Dataflows instead.
|
Dataflow2 |
Implementation of data flow analyses over user-supplied domains.
|
Dataflows |
Implementation of data flow analyses over user-supplied domains.
|
Datatype [State_builder.S] | |
Datatype [Service_graph.S.Service_graph] | |
Datatype [Project] | |
Datatype [Datatype.Caml_weak_hashtbl] | |
Datatype |
A datatype provides useful values for types.
|
Db |
Database in which static plugins are registered.
|
Debug [Plugin.S] | |
Debug_category [Plugin.S] |
prints debug messages having the corresponding key.
|
Debug_manager |
Nothing exported.
|
Descr |
Type descriptor for safe unmarshalling.
|
Description |
Describe items of Source and Properties.
|
Design |
The extensible GUI.
|
Destructors |
retrieve local variables with
__fc_destructor attribute and add
the appropriate calls to the corresponding destructor function when we
exit the scope of the variable.
|
Dir_name [Parameter_sig.Specific_dir] |
Option
-<short-name>-<specific-dir> .
|
DoCollapseCallCast [Kernel] |
Behavior of option "-collapse-call-cast".
|
Dominators |
Computation of dominators.
|
Dot [State_dependency_graph] | |
Dynamic |
Value accesses through dynamic typing.
|
E | |
Eid [Cil] | |
Emitted_status [Property_status] | |
Emitter |
Emitter.
|
Empty_string [Parameter_sig.Builder] | |
Enable [Kernel.Journal] |
Behavior of option "-journal-enable"
|
Enuminfo [Cil_datatype] | |
Enumitem [Cil_datatype] | |
Enums [Kernel] |
Behavior of option "-enums"
|
Errorloc |
The module stores the current file,line, and working directory in a
hidden internal state, modified by the three following
functions.
|
Escape |
OCaml types used to represent wide characters and strings
|
Exn_flow |
Manages information related to possible exceptions thrown by each
function in the AST.
|
Exp [Cil_datatype] |
Note that the equality is based on eid.
|
ExpStructEq [Cil_datatype] | |
Exp_hashtbl [Cil_state_builder] | |
Extlib |
Useful operations.
|
F | |
F [Fval] | |
F [Filter] |
Given a module that match the module type described above,
F.build_cil_file initializes a new project containing the slices
|
FCBuffer |
Extensible buffers.
|
FCHashtbl |
Extension of OCaml's
Hashtbl module.
|
FCMap |
Association tables over ordered types.
|
FCSet |
Sets over ordered types.
|
False [Parameter_sig.Builder] | |
False_ref [State_builder] |
Build a reference on a boolean, initialized with
false .
|
Feedback [Property_status] |
Lighter version than Consolidation
|
Feedback [Design] |
Bullets in left-margins
|
Fieldinfo [Cil_datatype] | |
File |
Frama-c preprocessing and Cil AST initialization.
|
File [Cil_datatype] | |
FileIndex [Globals] |
Globals associated to filename.
|
File_manager |
Nothing exported.
|
Filecheck |
This file performs various consistency checks over a cil file.
|
Filepath |
Functions manipulating filepaths.
|
Files [Kernel] |
Analyzed files
|
Filetree |
The tree containing the list of modules and functions together with dynamic columns
|
Filled_string_set [Parameter_sig.Builder] | |
Filter | Filter helps to build a new cilfile from an old one by removing some of
its elements.
|
Float [Datatype] | |
FloatHex [Kernel] |
Behavior of option "-float-hex"
|
FloatNormal [Kernel] |
Behavior of option "-float-normal"
|
FloatRelative [Kernel] |
Behavior of option "-float-relative"
|
Float_ref [State_builder] |
Build a reference on a float.
|
Floating_point |
Floating-point operations.
|
Fold [Hook] | |
Fold_ordered [Hook] | |
ForceRLArgEval [Kernel] |
Behavior of option "-force-rl-arg-eval".
|
Formatter [Datatype] | |
Forwards [Dataflow2] | |
Forwards [Dataflow] | |
FramaCStdLib [Kernel] |
Behavior of option "-frama-c-stdlib"
|
Frama_c_builtins [Cil] |
This module associates the name of a built-in function that might be used
during elaboration with the corresponding varinfo.
|
Frama_c_init |
Setting global, platform-wide settings.
|
From [Db] |
Functional dependencies between function inputs and function outputs.
|
Frontc |
Signals that we are in MS VC mode
|
Funbehavior [Cil_datatype] | |
Function [Type] |
Instance of
Type.Polymorphic2 for functions: same signature than
Type.Polymorphic2 with possibility to specify a label for the function
parameter.
|
Function [Datatype] | |
Function [Ast_info] |
Operations on cil function.
|
Functions [Globals] |
Functions.
|
Fundec [Cil_datatype] | |
Fundec_set [Parameter_sig.Builder] | |
Funspec [Cil_datatype] | |
Fval |
Floating-point intervals, used to construct arithmetic lattices.
|
G | |
G [State_dependency_graph.S] | |
GeneralDebug [Kernel] |
Behavior of option "-debug"
|
GeneralVerbose [Kernel] |
Behavior of option "-verbose"
|
Global [Cil_datatype] | |
Global_annotation [Cil_datatype] | |
Globals |
Operations on globals.
|
Group [Cmdline] |
Group of command line options.
|
Gtk_form |
DEPRECATED.
|
Gtk_helper |
Generic Gtk helpers.
|
Gui_init |
Very early initialisation step required by any GUI.
|
Gui_parameters |
GUI as a plug-in.
|
Gui_printers |
Special pretty-printers for the GUI.
|
H | |
Hashcons [State_builder] |
Hashconsed version of an arbitrary datatype
|
Hashconsing_tbl [State_builder] |
Weak or non-weak hashconsing tables, depending on variable
Cmdline.deterministic .
|
Hashconsing_tbl_not_weak [State_builder] |
Hash table for hashconsing, but the internal table is _not_ weak
(it is a regular hash table).
|
Hashconsing_tbl_weak [State_builder] |
Weak hashtbl dedicated to hashconsing.
|
Hashtbl [State_builder] | |
Hashtbl [Datatype] | |
Hashtbl [Datatype.S_with_collections] | |
Help [Plugin.S] | |
Help_manager |
Nothing exported.
|
History |
Source code navigation history.
|
Hook |
Hook builder.
|
Hptmap |
Efficient maps from hash-consed trees to values, implemented as
Patricia trees.
|
Hptmap_sig |
Signature for the
Hptmap module
|
Hptset [Kernel_function] |
Set of kernel functions.
|
Hptset |
Sets over ordered types.
|
Hptset [Cil_datatype.Varinfo] | |
Hptset [Cil_datatype.Stmt] | |
Hptset [Base] | |
I | |
Icon [Gtk_helper] |
Some generic icon management tools.
|
Identified_predicate [Cil_datatype] | |
Identified_term [Cil_datatype] | |
Impact [Db] |
Impact analysis.
|
ImplicitFunctionDeclaration [Kernel] |
Behavior of option "-implicit-function-declaration"
|
Indexer |
Indexer implements ordered collection of items with
random access.
|
Infer_annotations |
Generation of possible assigns from the C prototype of a function.
|
InitializedPaddingLocals [Kernel] |
Behavior of option "-initialized-padding-locals"
|
Initinfo [Cil_datatype] | |
Inputs [Db] |
State_builder.of read inputs.
|
Instr [Cil_datatype] | |
Int [Parameter_sig.Builder] | |
Int [Dynamic.Parameter] |
Integer parameters.
|
Int [Datatype] | |
Int [Abstract_interp] | |
Int32 [Datatype] | |
Int64 [Datatype] | |
Int_Base |
Big integers with an additional top element.
|
Int_Intervals |
Sets of intervals with a lattice structure.
|
Int_Intervals_sig |
Sets of intervals with a lattice structure.
|
Int_hashtbl [State_builder] | |
Int_ref [State_builder] |
Build a reference on an integer.
|
Integer |
Extension of
Big_int compatible with Zarith .
|
Integer [Datatype] | |
Interp [Db.Properties] |
Interpretation of logic terms.
|
Ival |
Arithmetic lattices.
|
J | |
Journal [Kernel] |
Kernel for journalization.
|
Journal |
Journalization of functions.
|
Json |
Json Library
|
K | |
KeepSwitch [Kernel] |
Behavior of option "-keep-switch"
|
Keep_unused_specified_functions [Kernel] |
Behavior of option "-keep-unused-specified-function".
|
Kernel |
Provided services for kernel developers.
|
Kernel_function |
Operations to get info from a kernel function.
|
Kernel_function_hashtbl [Cil_state_builder] | |
Kernel_function_map [Parameter_sig.Builder] |
As for Kernel_function_set, by default keys can only be defined functions.
|
Kernel_function_multiple_map [Parameter_sig.Builder] |
As for Kernel_function_set, by default keys can only be defined functions.
|
Kernel_function_set [Parameter_sig.Builder] | |
Key [Datatype.Hashtbl] |
Datatype for the keys of the hashtbl.
|
Key [Datatype.Map] |
Datatype for the keys of the map.
|
Kf [Cil_datatype] | |
Kinstr [Cil_datatype] | |
Kinstr_hashtbl [Cil_state_builder] | |
L | |
LOffset [Lmap_bitwise.Location_map_bitwise] | |
Label [Cil_datatype] | |
Lattice_messages |
Message and logging facility for abstract lattices.
|
Lattice_type |
Lattice signatures.
|
Launcher |
The Frama-C launcher.
|
Leftistheap |
Leftist heaps.
|
Lemmas [Logic_env] | |
Lenv [Logic_typing] |
Local logic environment
|
Lexerhack | |
Lexpr [Cil_datatype] | |
LibEntry [Kernel] |
Behavior of option "-lib-entry".
|
LinkPrinter [Gui_printers] |
Special pretty-printer that outputs tags
link:vidN around varinfos,
and link:typN around types.
|
List [Datatype] | |
List_ref [State_builder] |
Build a reference on a list.
|
List_with_collections [Datatype] | |
Lmap |
Maps from bases to memory maps.
|
Lmap_bitwise |
Functors making map indexed by zone.
|
Lmap_sig |
Signature for maps from bases to memory maps.
|
LoadModule [Kernel] |
Behavior of option "-load-module"
|
LoadState [Kernel] |
Behavior of option "-load"
|
Localisation [Cil_datatype] | |
Localizable [Pretty_source] | |
Location [Locations] | |
Location [Cil_datatype] |
Cil locations.
|
LocationSetLattice [Origin] |
Sets of source locations
|
Location_Bits [Locations] |
Association between bases and offsets in bits.
|
Location_Bytes [Locations] |
Association between bases and offsets in byte.
|
Locations |
Memory locations.
|
Locs [Pretty_source] | |
Log |
Logging Services for Frama-C Kernel and Plugins.
|
Logic [Db.Value] |
Evaluation of logic terms and predicates
|
Logic_builtin | |
Logic_builtin_used [Logic_env] |
logic function/predicates that are effectively used in current project.
|
Logic_const |
Smart constructors for logic annotations.
|
Logic_constant [Cil_datatype] | |
Logic_ctor_info [Logic_env] | |
Logic_ctor_info [Cil_datatype] | |
Logic_env |
Global Logic Environment
|
Logic_info [Logic_env] |
Global Tables
|
Logic_info [Cil_datatype] | |
Logic_interp |
All the interesting functions of this module are exported through
Db.Interp .
|
Logic_label [Cil_datatype] | |
Logic_lexer | |
Logic_parser | |
Logic_preprocess |
adds another pre-processing step in order to expand macros in
annotations.
|
Logic_print |
Pretty-printing of a parsed logic tree.
|
Logic_ptree |
logic constants.
|
Logic_type [Cil_datatype] |
Logic_type.
|
Logic_type_ByName [Cil_datatype] | |
Logic_type_NoUnroll [Cil_datatype] | |
Logic_type_info [Logic_env] | |
Logic_type_info [Cil_datatype] | |
Logic_typing |
Logic typing and logic environment.
|
Logic_utils |
Utilities for ACSL constructs.
|
Logic_var [Cil_datatype] | |
Loop |
Operations on (natural) loops.
|
Lval [Cil_datatype] |
Note that the equality is based on eid (for sub-expressions).
|
LvalStructEq [Cil_datatype] | |
M | |
M [Map_Lattice.Make_without_cardinal] | |
M [Locations.Location_Bytes] | |
MAKE_CUSTOM_LIST [Gtk_helper] |
A functor to build custom Gtk lists.
|
Machdep [Kernel] |
Behavior of option "-machdep".
|
Machdeps |
Some predefined
Cil_types.mach which specifies machine-dependent
data about C programs.
|
Main [Db] |
Frama-C main interface.
|
MainFunction [Kernel] |
Behavior of option "-main".
|
Make [Wto] |
This functor provides the partitioning algorithm constructing a WTO.
|
Make [State_topological] |
Functor providing topological iterators over a graph.
|
Make [Service_graph] |
Generic functor implementing the services algorithm according to a graph
implementation.
|
Make [Rangemap] |
Extension of the above signature, with specific functions acting
on range of values
|
Make [Qstack] | |
Make [Printer_builder] | |
Make [Parameter_builder] | |
Make [Offsetmap] |
Maps from intervals to values.
|
Make [Map_Lattice] | |
Make [Logic_typing] | |
Make [Leftistheap] | |
Make [Indexer] | |
Make [Hptset] | |
Make [Hptmap] | |
Make [Hook] |
Make a new empty hook from
unit .
|
Make [FCSet] |
Functor building an implementation of the set structure
given a totally ordered type.
|
Make [FCMap] |
Functor building an implementation of the map structure
given a totally ordered type.
|
Make [FCHashtbl] | |
Make [Datatype.Polymorphic4] | |
Make [Datatype.Polymorphic3] | |
Make [Datatype.Polymorphic2] | |
Make [Datatype.Polymorphic] |
Create a datatype for a monomorphic instance of the polymorphic type.
|
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 [Datatype] |
Generic datatype builder.
|
Make_Datatype [Bottom] |
Datatype constructor.
|
Make_Hashconsed_Lattice_Set [Abstract_interp] |
See e.g.
|
Make_LOffset [Lmap] | |
Make_Lattice_Base [Abstract_interp] | |
Make_Lattice_Product [Abstract_interp] |
If
C.collapse then L1.bottom,_ = _,L2.bottom = bottom
|
Make_Lattice_Set [Abstract_interp] | |
Make_Lattice_Sum [Abstract_interp] | |
Make_Lattice_UProduct [Abstract_interp] |
Uncollapsed product.
|
Make_Narrow [Offsetmap_sig] | |
Make_Narrow [Lmap_sig] | |
Make_Table [Kernel_function] |
Hashtable indexed by kernel functions and dealing with project.
|
Make_bitwise [Offsetmap] |
Maps from intervals to simple values.
|
Make_bitwise [Lmap_bitwise] | |
Make_list [Parameter_sig.Builder] | |
Make_map [Parameter_sig.Builder] |
Parameter is a map where multibindings are **not** allowed.
|
Make_multiple_map [Parameter_sig.Builder] |
Parameter is a map where multibindings are allowed.
|
Make_ordered [Hook] | |
Make_set [Parameter_sig.Builder] | |
Make_setter [Project_skeleton] | |
Make_table [Emitter] |
Table indexing: key -> emitter (or equivalent data) -> value.
|
Make_tbl [Type] |
Build an heterogeneous table associating keys to info.
|
Make_with_collections [Datatype] |
Generic comparable datatype builder: functions
equal , compare and
hash must not be Datatype.undefined .
|
Make_without_cardinal [Map_Lattice] | |
Map [Datatype] | |
Map [Datatype.S_with_collections] | |
Map_Lattice |
Map from a set of keys to values (a
Lattice_With_Diff ), equipped
with the natural lattice interpretation.
|
Mark [Db.Slicing] |
Access to slicing results.
|
Menu_manager |
Handle the menubar and the toolbar.
|
Mergecil |
Merge a number of CIL files
|
Messages |
Stored messages for persistence between sessions.
|
Model_info [Logic_env] | |
Model_info [Cil_datatype] | |
N | |
Name [Kernel.Journal] |
Behavior of option "-journal-name"
|
Names [Property] | |
Nativeint [Datatype] | |
O | |
O [Lattice_type.Lattice_Set] | |
O [Lattice_type.Lattice_Set_Generic] | |
O [Lattice_type.Lattice_Hashconsed_Set] | |
Obj_tbl [Type] |
Heterogeneous table for the keys, but polymorphic for the values.
|
Occurrence [Db] |
Interface for the occurrence plugin.
|
Offset [Cil_datatype] |
Same remark as for Lval.
|
OffsetStructEq [Cil_datatype] | |
Offsetmap |
Maps from intervals to values.
|
Offsetmap_bitwise_sig |
Signature for
Offsetmap_bitwise module, that implement efficient maps
from intervals to values.
|
Offsetmap_lattice_with_isotropy |
Type of the arguments of functor
Offsetmap.Make
|
Offsetmap_sig |
Signature for
Offsetmap module, that implement efficient maps from
intervals to arbitrary values.
|
Oneret |
Make sure that there is only one Return statement in the whole body.
|
Operational_inputs [Db] |
State_builder.of operational inputs.
|
Option [Datatype] | |
Option_ref [State_builder] |
Build a reference on an option.
|
Option_with_collections [Datatype] | |
Ordered_stmt |
An
ordered_stmt is an int representing a stmt in a particular
function.
|
Orig_name [Kernel] |
Behavior of option "-orig-name"
|
Origin |
The datastructures of this module can be used to track the origin
of a major imprecision in the values of an abstract domain.
|
Output [Project_skeleton] | |
Outputs [Db] |
State_builder.of outputs.
|
P | |
Pair [Datatype] | |
Pair_with_collections [Datatype] | |
Parameter [Dynamic] |
Module to use for accessing parameters of plug-ins.
|
Parameter_builder |
Functors for implementing new command line options.
|
Parameter_category |
Category for parameter collections.
|
Parameter_customize |
Configuration of command line options.
|
Parameter_sig |
Signatures for command line options.
|
Parameter_state |
Handling groups of parameters
|
Pdg [Db] |
Program Dependence Graph.
|
Plugin |
Provided plug-general services for plug-ins.
|
Poly_array [Datatype] | |
Poly_list [Datatype] | |
Poly_option [Datatype] | |
Poly_pair [Datatype] | |
Poly_queue [Datatype] | |
Poly_ref [Datatype] | |
Polymorphic [Type] |
Generic implementation of polymorphic type value.
|
Polymorphic [Datatype] |
Functor for polymorphic types with only 1 type variable.
|
Polymorphic2 [Type] |
Generic implementation of polymorphic type value with two type variables.
|
Polymorphic2 [Datatype] |
Functor for polymorphic types with 2 type variables.
|
Polymorphic3 [Type] |
Generic implementation of polymorphic type value with three type
variables.
|
Polymorphic3 [Datatype] |
Functor for polymorphic types with 3 type variables.
|
Polymorphic4 [Type] |
Generic implementation of polymorphic type value with four type
variables.
|
Polymorphic4 [Datatype] |
Functor for polymorphic types with 4 type variables.
|
Position [Cil_datatype] |
Single position in a file.
|
Postdominators [Db] |
Syntactic postdominators plugin.
|
PostdominatorsTypes [Db] |
Declarations common to the various postdominators-computing modules
|
PostdominatorsValue [Db] |
Postdominators using value analysis results.
|
Predicate [Cil_datatype] | |
PreprocessAnnot [Kernel] |
Behavior of option "-pp-annot"
|
Pretty_source |
Utilities to pretty print source with located elements in a Gtk
TextBuffer.
|
Pretty_utils |
Pretty-printer utilities.
|
PrintCode [Kernel] |
Behavior of option "-print"
|
PrintComments [Kernel] |
Behavior of option "-keep-comments"
|
PrintConfig [Kernel] |
Behavior of option "-print-config"
|
PrintLib [Kernel] |
Behavior of option "-print-lib-path"
|
PrintLibc [Kernel] |
Behavior of option "-print-libc"
|
PrintMachdep [Kernel] |
Behavior of option "-print-machdep"
|
PrintPluginPath [Kernel] |
Behavior of option "-print-plugin-path"
|
PrintShare [Kernel] |
Behavior of option "-print-share-path"
|
PrintVersion [Kernel] |
Behavior of option "-print-version"
|
Printer |
AST's pretty-printer.
|
Printer_api |
Type of AST's extensible printers.
|
Printer_builder |
Build a full pretty-printer from a pretty-printing class.
|
Project |
Projects management.
|
Project [Db.Slicing] |
Slicing project management.
|
Project_manager |
No function is exported.
|
Project_name [Gui_parameters] |
Option -gui-project.
|
Project_skeleton |
This module should not be used outside of the Project library.
|
Properties [Db] |
Dealing with logical properties.
|
Property |
ACSL comparable property.
|
Property_navigator |
Extension of the GUI in order to navigate in ACSL properties.
|
Property_status |
Status of properties.
|
Proxy [State_builder] |
State proxy.
|
Q | |
Qstack |
Mutable stack in which it is possible to add data at the end (like a queue)
and to handle non top elements.
|
Quadruple [Datatype] | |
Quadruple_with_collections [Datatype] | |
Queue [State_builder] | |
Queue [Datatype] | |
Quiet [Kernel] |
Behavior of option "-quiet"
|
R | |
Rangemap |
Association tables over ordered types.
|
ReadAnnot [Kernel] |
Behavior of option "-read-annot"
|
Record_From_Callbacks [Db.From] | |
Record_Value_After_Callbacks [Db.Value] | |
Record_Value_Callbacks [Db.Value] | |
Record_Value_Superposition_Callbacks [Db.Value] | |
Recursive [Structural_descr] |
Use this module for handling a (possibly recursive) structural descriptor
d .
|
Ref [State_builder] | |
Ref [Datatype] | |
Register [State_builder] | Register(Datatype)(State)(Info) registers a new state.
|
Register [Plugin] |
Functors for registering a new plug-in.
|
Register [Log] |
Each plugin has its own channel to output messages.
|
Rel [Abstract_interp] |
"Relative" integers.
|
RemoveExn [Kernel] |
Behavior of option "-remove-exn"
|
Report [Db] |
Dump Properties-Status consolidation tree.
|
Request [Db.Slicing] |
Requests for slicing jobs.
|
Reverse_binding [Journal] | |
Rgmap |
Associative maps for _ranges_ to _values_ with overlapping.
|
Rmtmps |
removes unused labels for which
is_removable is true.
|
RteGen [Db] |
Runtime Error Annotation Generation plugin.
|
S | |
SafeArrays [Kernel] |
Behavior of option "-safe-arrays".
|
SaveState [Kernel] |
Behavior of option "-save"
|
Scope [Db] |
Interface for the Scope plugin.
|
Security [Db] |
Security analysis.
|
Select [Db.Slicing] |
Slicing selections.
|
Serializable_undefined [Datatype] |
Same as
Datatype.Undefined , but the type is supposed to be marshallable by the
standard OCaml way (in particular, no hash-consing or projects inside
the type).
|
Service_graph [Service_graph.S] | |
Service_graph |
Compute services from a callgraph.
|
Session [Plugin.S] |
Handle the specific `session' directory of the plug-in.
|
Session_dir [Kernel] |
Directory in which session files are searched.
|
Set [Datatype] | |
Set [Datatype.S_with_collections] | |
SetLattice [Base] | |
Set_project_as_default [Kernel] |
Undocumented.
|
Set_ref [State_builder] | |
Shape [Hptmap] |
This functor exports the shape of the maps indexed by keys
Key .
|
Share [Plugin.S] |
Handle the specific `share' directory of the plug-in.
|
SharedCounter [State_builder] |
Creates a counter that is shared among all projects, but which is
marshalling-compliant.
|
Sid [Cil] | |
SignedDowncast [Kernel] |
Behavior of option "-warn-signed-downcast"
|
SignedOverflow [Kernel] |
Behavior of option "-warn-signed-overflow"
|
Simple_backward [Dataflows] | |
Simple_forward [Dataflows] | |
SimplifyCfg [Kernel] |
Behavior of option "-simplify-cfg"
|
SimplifyTrivialLoops [Kernel] |
Behavior of option "-simplify-trivial-loops".
|
Slice [Db.Slicing] |
Function slice.
|
Slicing [Db] |
Interface for the slicing tool.
|
Source_manager |
The source viewer multi-tabs widget window.
|
Source_viewer |
The Frama-C source viewer.
|
Sparecode [Db] |
Interface for the unused code detection.
|
Special_hooks |
Nothing is exported: just register some special hooks for Frama-C.
|
StartData [Dataflow2] |
This module can be used to instantiate the
StmtStartData components
of the functors below.
|
StartData [Dataflow] |
This module can be used to instantiate the
StmtStartData components
of the functors below.
|
State |
A state is a project-compliant mutable value.
|
State_builder |
State builders.
|
State_dependency_graph |
State Dependency Graph.
|
State_selection |
A state selection is a set of states with operations for easy handling of
state dependencies.
|
State_topological |
Topological ordering over states.
|
States [State_builder] | |
Static [State_selection] |
Operations over selections which depend on
State_dependency_graph.graph .
|
Statuses_by_call |
Statuses of preconditions specialized at a given call-point.
|
Stmt [Cil_datatype] | |
StmtStartData [Dataflow2.BackwardsTransfer] |
For each block id, the data at the start.
|
StmtStartData [Dataflow2.ForwardsTransfer] |
For each statement id, the data at the start.
|
StmtStartData [Dataflow.BackwardsTransfer] |
For each block id, the data at the start.
|
StmtStartData [Dataflow.ForwardsTransfer] |
For each statement id, the data at the start.
|
Stmt_Id [Cil_datatype] | |
Stmt_hashtbl [Cil_state_builder] | |
Stmt_set_ref [Cil_state_builder] | |
Stmts_graph |
Statements graph.
|
String [Transitioning] |
In OCaml 4.03, many functions
f from String have been deprecated
in favor of f_ascii , which operate only on the ASCII charset, while
the deprecated f knew about iso-8859-1.
|
String [Parameter_sig.Builder] | |
String [Dynamic.Parameter] |
String parameters.
|
String [Datatype] | |
StringList [Dynamic.Parameter] |
List of string parameters.
|
StringSet [Dynamic.Parameter] |
Set of string parameters.
|
String_list [Parameter_sig.Builder] | |
String_map [Parameter_sig.Builder] | |
String_multiple_map [Parameter_sig.Builder] | |
String_set [Parameter_sig.Builder] | |
String_tbl [Type] |
Heterogeneous tables indexed by string.
|
Structural_descr |
Internal representations of OCaml type as first class values.
|
SymbolicPath [Kernel] |
Behavior of option "-add-symbolic-path"
|
Symmetric_Binary [Binary_cache] | |
Symmetric_Binary_Predicate [Binary_cache] | |
T | |
TP [Service_graph.S] | |
Table_By_Callstack [Db.Value] |
Table containing the results of the value analysis, ie.
|
Task |
High Level Interface to Command.
|
Term [Cil_datatype] | |
Term_lhost [Cil_datatype] | |
Term_lval [Cil_datatype] | |
Term_offset [Cil_datatype] | |
Theme [Gui_parameters] |
Option -gui-theme.
|
Time [Kernel] |
Behavior of option "-time"
|
To_zone [Logic_interp] | |
To_zone [Db.Properties.Interp] | |
Top [Bottom] |
Lattices in which both top and bottom are managed separately
|
Top_Param [Map_Lattice.Make_without_cardinal] | |
Toplevel [Db] | |
Tr_offset |
Reduction of a location (expressed as an Ival.t and a size)
by a base validity.
|
Transitioning |
This file contains functions that uses features that are deprecated in
current OCaml version, but whose replacing feature is not available in
the oldest OCaml version officially supported by Frama-C.
|
Translate_lightweight |
Annotate files interpreting lightweight annotations.
|
Triple [Datatype] | |
Triple_with_collections [Datatype] | |
True [Parameter_sig.Builder] | |
True_ref [State_builder] |
Build a reference on a boolean, initialized with
true .
|
Ty_tbl [Type] |
Heterogeneous tables indexed by type value.
|
Typ [Cil_datatype] |
Types, with comparison over struct done by key and unrolling of typedefs.
|
TypByName [Cil_datatype] |
Types, with comparison over struct done by name and no unrolling.
|
TypNoUnroll [Cil_datatype] |
Types, with comparison over struct done by key and no unrolling
|
Type |
Type value.
|
Type [Bottom] | |
TypeCheck [Kernel] |
Behavior of option "-typecheck"
|
Type_namespace [Logic_typing] | |
Typed_parameter |
Parameter settable through a command line option.
|
Typeinfo [Cil_datatype] | |
Types [Globals] |
Types, or type-related information.
|
U | |
Undefined [Datatype] |
Each values in these modules are undefined.
|
Undefined_sequence | |
Undo [Project] | |
Undo [Gui_parameters] |
Option -undo.
|
Unicode |
Handling unicode string.
|
Unicode [Kernel] |
Behavior of option "-unicode".
|
Unit [Datatype] | |
Unmarshal |
Provides a function
input_val , similar in
functionality to the standard library function Marshal.from_channel .
|
Unmarshal_z | |
Unroll_loops |
Syntactic loop unrolling.
|
UnrollingForce [Kernel] |
Behavior of option "-ulevel-force"
|
UnrollingLevel [Kernel] |
Behavior of option "-ulevel"
|
UnsignedDowncast [Kernel] |
Behavior of option "-warn-unsigned-downcast"
|
UnsignedOverflow [Kernel] |
Behavior of option "-warn-unsigned-overflow"
|
UnspecifiedAccess [Kernel] |
Behavior of option "-unspecified-access"
|
UntypedFiles [Ast] | |
Usable_emitter [Emitter] |
Usable emitters are the ones which can really emit something.
|
UseUnicode [Kernel] |
Behavior of option "-unicode"
|
Users [Db] |
Functions used by another function.
|
Utf8_logic |
UTF-8 string for logic symbols.
|
V | |
Validity [Base] | |
Value [Db] |
The Value analysis itself.
|
Varinfo [Cil_datatype] | |
Varinfo_Id [Cil_datatype] | |
Varinfo_hashtbl [Cil_state_builder] | |
Vars [Globals] |
Globals variables.
|
Vector |
Extensible Arrays
|
Verbose [Plugin.S] | |
Vid [Cil_const] | |
Visitor |
Frama-C visitors dealing with projects.
|
W | |
WTO [Wto_statement] |
The datatype for statement WTOs
|
WTOIndex [Wto_statement] |
Datatype for wto_index
|
WarnDecimalFloat [Kernel] |
Behavior of option "-warn-decimal-float"
|
Warning_manager |
Handle Frama-C warnings in the GUI.
|
Wbox |
Box Layouts.
|
Weak [Datatype] | |
Weak_hashtbl [State_builder] |
Build a weak hashtbl over a datatype
Data from a reference implementation
W .
|
Wfile |
File Choosers
|
Wide_string [Cil_datatype] | |
Widen_Hints [Ival] | |
Widget |
Simple Widgets
|
WithOutput [Parameter_sig.Builder] | |
With_collections [Datatype] |
Add sets, maps and hashtables modules to an existing datatype, provided the
equal , compare and hash functions are not Datatype.undefined .
|
Wpalette |
A side-bar palette of tools.
|
Wpane |
Panels
|
Wtable |
Table Views
|
Wtext |
Rich Text Renderer
|
Wto |
Weak topological orderings (WTOs) are a hierarchical decomposition of the
a graph where each layer is topologically ordered and strongly connected
components are aggregated and ordered recursively.
|
Wto_statement |
Specialization of WTO for the CIL statement graph.
|
Wutil |
Wtoolkit - Utilities
|
Z | |
Zero [Parameter_sig.Builder] | |
Zero_ref [State_builder] |
Build a reference on an integer, initialized with
0 .
|
Zone [Locations] |
Association between bases and ranges of bits.
|