Index of modules


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.