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.
Acsl_extension
ACSL extensions registration module
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"
Automaton [Interpreted_automata]
Datatype for automata

B
Backwards [Dataflow2]
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_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.
Cfg
Code to compute the control-flow graph of a function or file.
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 [Interpreted_automata]
This module defines the previous functions without memoization
Compute_Statement_Callbacks [Db.Value]
Actions to perform whenever a statement is handled.
Config [Plugin.S_no_log]
Handle the specific `config' directory of the plug-in.
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.
Constant [Cil_datatype]
Constfold [Kernel]
Behavior of option "-constfold"
ContinueOnAnnotError [Kernel]
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"
CppExtraArgsPerFile [Kernel]
Behavior of option "-cpp-extra-args-per-file"
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.

D
Dataflow [Interpreted_automata]
Builds a simple dataflow analysis over an input domain.
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_no_log]
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.
Dgraph_helper
Create a new window displaying a graph.
DoCollapseCallCast [Kernel]
Behavior of option "-collapse-call-cast".
Dominators
Computation of dominators.
Dot [State_dependency_graph]
Dotgraph
Helper for Printing Dot-graphs.
Dynamic
Value accesses through dynamic typing.
Dynlink [Transitioning]
4.08

E
Edge [Interpreted_automata]
Eid [Cil_const]
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
Eva_lattice_type
Lattice signatures using the Bottom type: these lattices do not include a bottom element, and return `Bottom instead when needed.
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
FCHashtbl
Extension of OCaml's Hashtbl module.
False [Parameter_sig.Builder]
False_ref [State_builder]
Build a reference on a boolean, initialized with false.
Fc_Filepath [Parameter_sig.Builder]
Fc_config
Information about version of Frama-C.
Fc_float
Implementation of floating-point values of different precision, using the standard ocaml floating-point numbers in double precision.
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 [Parameter_sig.Builder]
Filepath
Functions manipulating filepaths.
Filepath [Dynamic.Parameter]
Filepath parameters.
Filepath [Datatype]
Type-safe strings representing normalized filepaths.
Filepath_list [Parameter_sig.Builder]
Filepath_map [Parameter_sig.Builder]
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 [Transitioning]
4.07
Float [Datatype]
FloatHex [Kernel]
Behavior of option "-float-hex"
FloatNormal [Kernel]
Behavior of option "-float-normal"
FloatRelative [Kernel]
Behavior of option "-float-relative"
Float_interval
Builds a semantics of floating-point intervals for different precisions, from a module providing the floating-point numbers used for the bounds of the intervals.
Float_interval_sig
Signature for the floating-point interval semantics.
Float_ref [State_builder]
Build a reference on a float.
Float_sig
Interface of floating-point numbers of different precisions.
Floating_point
Floating-point operations.
Fold [Visitor_behavior]
Fold operations on table of a given type of AST elements.
Fold [Hook]
Fold_ordered [Hook]
Format [Transitioning]
4.08
Formatter [Datatype]
Forwards [Dataflow2]
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]
G [Interpreted_automata.UnrollUnnatural]
G [Interpreted_automata]
GSourceView
GeneralDebug [Kernel]
Behavior of option "-debug"
GeneralVerbose [Kernel]
Behavior of option "-verbose"
Get [Visitor_behavior]
Get operations on behaviors, allows to get the representative of an AST element in the current state of the visitor.
Get_orig [Visitor_behavior]
Get operations on behaviors, allows to get the original representative of an element of the new AST in the curent state of the visitor.
Ghost_accesses
Checks that memory accesses are well-typed in the sense of the \ghost qualifier.
Ghost_cfg
Checks that normal cfg is not altered by ghost statements.
Global [Cil_datatype]
Global_annotation [Cil_datatype]
Globals
Operations on globals.
Group [Cmdline]
Group of command line options.
Gtk_compat
makes the font smaller.
Gtk_form
DEPRECATED.
Gtk_helper
Generic Gtk helpers.
Gui_init
Very early initialization 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_no_log]
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]
ImplicitFunctionDeclaration [Kernel]
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]
Inline
inline_term ~inline term inlines in term the application of predicates and logic functions for which inline is true.
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_interval
Integer intervals with congruence.
Int_ref [State_builder]
Build a reference on an integer.
Int_set
Small sets of integers.
Int_val
Integer values abstractions: an abstraction represents a set of integers.
Integer
Extension of Big_int compatible with Zarith.
Integer [Datatype]
Interp [Db.Properties]
Interpretation of logic terms.
Interpreted_automata
An interpreted automaton is a convenient formalization of programs for abstract interpretation.
InvalidBool [Kernel]
Behavior of option "-warn-invalid-bool"
InvalidPointer [Kernel]
Behavior of option "-warn-invalid-pointer"
Iter [Visitor_behavior]
Iter operations on the table of a given type of AST elements.
Ival
Arithmetic lattices.

J
Journal [Kernel]
Kernel for journalization.
Journal
Journalization of functions.
Json
Json Library
JsonCompilationDatabase [Kernel]
Behavior of option "-json-compilation-database"
Json_compilation_database
get_flags f returns the preprocessing flags associated to file f in the JSON compilation database (when enabled), or the empty string otherwise.

K
KeepSwitch [Kernel]
Behavior of option "-keep-switch"
Keep_unused_specified_functions [Kernel]
Behavior of option "-keep-unused-specified-functions".
Keep_unused_types [Kernel]
Behavior of option "-keep-unused-types".
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]
Kernel_function_set [Kernel]
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.
LeftShiftNegative [Kernel]
Behavior of option "-warn-left-shift-negative"
LegacyNames [Property]
Lemmas [Logic_env]
Lenv [Logic_typing]
Local logic environment
Lexerhack
Lexpr [Cil_datatype]
Beware: no pretty-printer is available.
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 [Printer_tag]
Location [Locations]
Location [Cil_datatype]
Cil locations.
LocationLattice [Origin]
Lattice 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_info_structural [Cil_datatype]
Logic_info with structural comparison: name of the symbol, type of arguments Note that polymorphism is ignored, in the sense that two symbols with the same name and profile except for the name of their type variables will compare unequal.
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_real [Cil_datatype]
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]
LogicalOperators [Kernel]
Behavior of invisible option -keep-logical operator: Tries to avoid converting && and || into conditional statements.
Loop
Operations on (natural) loops.
Lval [Cil_datatype]
Note that the equality is based on eid (for sub-expressions).
LvalStructEq [Cil_datatype]
Lval_hashtbl [Cil_state_builder]

M
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_tag]
Make [Printer_builder]
Make [Parameter_builder]
Make [Offsetmap]
Maps from intervals to values.
Make [Logic_typing]
Make [Indexer]
Make [Hptset]
Make [Hptmap]
Make [Hook]
Make a new empty hook from unit.
Make [Float_interval]
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]
Generic datatype builder.
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 [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_MapSet_Lattice [Map_lattice]
Builds a lattice mixing maps and sets, provided that each one has a lattice structure.
Make_Map_Lattice [Map_lattice]
Equips an Hptmap with a lattice structure, provided that the values have a lattice structure.
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_pp [Printer_builder]
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.
Map [Transitioning.Stdlib]
Map [Datatype]
Map [Datatype.S_with_collections]
Map_lattice
Maps equipped with a lattice structure.
Markdown
Markdown Document Structured representation of Markdown content.
Memo [Visitor_behavior]
Memo operations on behaviors, allows to get a binding in the new project for the given AST element, creating one if it does not already exists.
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]
Node [Dotgraph]
Lazily associates a node to any element.
Normalized [Filepath]
The Normalized module is simply a wrapper that ensures that paths are always normalized.

O
O [Lattice_type.Lattice_Set]
Obj_tbl [Type]
Heterogeneous table for the keys, but polymorphic for the values.
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
If there are local variables with destructors belonging to the main block of f, encapsulate_local_vars f will move ret, the return statement of f outside of this main block (changing f.sbody to a two-statement block composed of the old block and ret) to avoid having gotos to ret bypassing the initialization of these variables.
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]
Pango [Gtk_compat]
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
Special signature for Kernel services, whose messages are handled in an ad'hoc manner.
PointerDowncast [Kernel]
Behavior of option "-warn-pointer-downcast"
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"
PrintReturn [Kernel]
Behavior of option "-print-return"
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 dynamic printer that bind all pretty-printers to the object obtained by (P())
Printer_tag
Utilities to pretty print source with located Ast elements
Project
Projects 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
Q [Transitioning]
Function Q.to_float was introduced in Zarith 1.5
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 [Dotgraph]
Complex node layout.
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"
Reset [Visitor_behavior]
Reset operations on behaviors, allows to reset the tables associated to a given kind of AST elements.
Reverse_binding [Journal]
Rgmap
Associative maps for _ranges_ to _values_ with overlapping.
Rich_text
Text with Tags
RightShiftNegative [Kernel]
Behavior of option "-warn-right-shift-negative"
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".
Sanitizer
Sanitizer
SaveState [Kernel]
Behavior of option "-save"
Security [Db]
Security analysis.
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_no_log]
Handle the specific `session' directory of the plug-in.
Session_dir [Kernel]
Directory in which session files are searched.
Set [Visitor_behavior]
Set operations on behaviors, allows to change the representative of a given AST element in the current state of the visitor.
Set [Transitioning.Stdlib]
Set [Datatype]
Set [Datatype.S_with_collections]
SetLattice [Base]
Set_orig [Visitor_behavior]
Set operations on behaviors related to original representatives, allows to change the reference of an element of the new AST in the current state of the visitor.
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_no_log]
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_const]
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".
Source_manager
The source viewer multi-tabs widget window.
Source_viewer
The Frama-C source viewer.
SpecialFloat [Kernel]
Behavior of option "-warn-special-float"
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.
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.
Stdlib [Transitioning]
4.08
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.
Stmt_Id [Cil_datatype]
Stmt_hashtbl [Cil_state_builder]
Stmt_set_ref [Cil_state_builder]
Stmts_graph
Statements graph.
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.
Substitute_const_globals
A visitor that substitutes globals, defined with the attribute 'const', with respective initializers.
SymbolicPath [Kernel]
Behavior of option "-add-symbolic-path"
Symmetric_Binary [Binary_cache]
Symmetric_Binary_Predicate [Binary_cache]
Syntactic_scope [Cil_datatype]
Syntactic_search [Globals]

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]
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
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
UnrollUnnatural [Interpreted_automata]
Unroll_loops
Syntactic loop unrolling.
UnrollingForce [Kernel]
Behavior of option "-ulevel-force"
UnrollingLevel [Kernel]
Behavior of option "-ulevel"
Unset [Visitor_behavior]
Operations to remove the entry associated to a given AST element in the current state of the visitor.
Unset_orig [Visitor_behavior]
Operations to remove the entry associated to a given element of the new AST in the current state of the visitor.
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"
Utf8_logic
UTF-8 string for logic symbols.
UtilsFilepath [Cil_datatype]

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_no_log]
Version [Interpreted_automata.UnrollUnnatural]
Vertex [Interpreted_automata]
Datatype for vertices
Vertex_Set [Interpreted_automata.UnrollUnnatural]
Vid [Cil_const]
Visitor
Frama-C visitors dealing with projects.
Visitor_behavior
Operations on visitor behaviors.

W
WTO [Wto_statement]
The datatype for statement WTOs
WTO [Interpreted_automata.UnrollUnnatural]
WTO [Interpreted_automata]
WTOIndex [Wto_statement]
Datatype for wto_index
WTOIndex [Interpreted_automata]
Datatype for wto_index
WarnDecimalFloat [Kernel]
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]
Widen_Hints [Int_val]
Widen_Hints [Float_sig.S]
Widget
Simple Widgets
WithOutput [Parameter_sig.Builder]
With_Cardinality [Map_lattice.Make_MapSet_Lattice]
With_Cardinality [Map_lattice.Make_Map_Lattice]
Adds cardinality functions for maps, according to a notion of cardinality on the values.
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
Wutil_once
once f returns a function that will only be applied once per execution of the program and returns the same value afterwards.

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.