Index of modules


A
AE [Availexpslv]
AELV [Rmciltmps]
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.
Access_path [Db]
Do not use yet.
Action [Parameter_sig.Builder]
AddPath [Kernel]
Behavior of option "-add-path"
AfterTable [Db.Value]
Table containing the state of the value analysis after the evaluation of each reachable and evaluable statement.
AgressiveMerging [Kernel]
Behavior of option "-agressive-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.
Array [Datatype]
Array_with_collections [Datatype]
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]
AvailableExps [Availexpslv]
Availexpslv

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"
Big_int [Datatype]
Binary_cache
Very low-level abstract functorial caches.
Binding [Journal]
Bit_utils
Some bit manipulations.
Bitvector
Bitvector naive implementation.
Block [Cil_datatype]
Bool [Parameter_sig.Builder]
Bool [Dynamic.Parameter]
Boolean parameters.
Bool [Datatype]
Bool_ref [State_builder]
Build a reference on a boolean.
Buckx
Undocumented.
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
Cabs
This file was originally part of Hugues Casee's frontc 2.0, and has been extensively changed since.
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]
Cabsbranches
Force the link for branches
Cabscond
Interface to be used during Cabs2cil
Cabshelper
Helper functions for Cabs
Cabsvisit
Variable or function prototype name
CallG [Service_graph.Make]
Call_Value_Callbacks [Db.Value]
Actions to perform at each treatment of a "call" statement.
Callgraph
Compute a static call graph.
Callsite [Value_types]
Callstack [Value_types]
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_set [Log]
sets of category keywords
Cfg
Code to compute the control-flow graph of a function or file.
Char [Datatype]
Check [Kernel.Files]
Behavior of option "-check"
Cil
CIL main API.
CilE
CIL Extension for Frama-C.
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.
Cilconfig
Reading and storing configuration files from the filesystem.
Cilmsg
CIL's internal stack of errors.
Clexer
The C Lexer.
Cmdline
Command line parsing.
CodeOutput [Kernel]
Behavior of option "-ocode".
Code_annotation [Cil_datatype]
Collect_messages [Kernel]
Behavior of option "-collect-messages"
Command
Useful high-level system operations.
Comments [Cabshelper]
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.
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.Files]
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"
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.
Custom [Gtk_helper]
Simple and high level custom model interface
Cvalue
Representation of Value's abstract memory.

D
DF [Reachingdefs]
Dataflow
A framework for implementing data flow analysis.
Dataflow2
A framework for implementing data flow analysis.
Dataflows
Datatype [State_builder.S]
Datatype [Service_graph.Make.CallG]
Datatype [Project]
Datatype [Datatype.Caml_weak_hashtbl]
Datatype
A datatype provides useful values for types.
Db
Database in which static plugins are registered.
Deadcodeelim
Dead code elimination.
Debug [Plugin.S]
Debug_category [Plugin.S]
prints debug messages having the corresponding key.
Debug_level [Cmdline]
Debug_manager
Nothing exported.
Default_offsetmap [Cvalue]
Values bound by default to a variable.
Deps [Function_Froms]
Descr
Type descriptor for safe unmarshalling.
Description
Describe items of Source and Properties.
Design
The extensible GUI.
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
Dynamic plug-ins: registration and use.
Dynlink [Kernel]
Behavior of option "-dynlink"
Dynlink_common_interface
Wrapper for Dynlink compatible with all OCaml versions.

E
Eid [Cil]
Emitted_status [Property_status]
Emitter
Emitter.
EmptyString [Parameter_sig.Builder]
Enable [Kernel.Journal]
Behavior of option "-journal-enable"
Enuminfo [Cil_datatype]
Enumitem [Cil_datatype]
Enums [Kernel]
Behavior of option "-enums"
Errorloc
This function is used especially when the preprocessor has generated linemarkers in the output that let us know the current working directory at the time of preprocessing (option -fworking-directory for GNU CPP).
Escape
OCaml types used to represent wide characters and strings
Exp [Cil_datatype]
Note that the equality is based on eid.
ExpStructEq [Cil_datatype]
Expcompare
Extlib
Useful operations.

F
F [Ival]
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.
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 at 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.
Filepath
Functions manipulating filepaths.
Files [Kernel]
Analyzed files
Filetree
The tree containing the list of modules and functions together with dynamic columns
FilledStringSet [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_abstract [Ival]
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]
Frama_c_builtins [Cil]
This module associates the name of a built-in function that might be used during elaboration with the corresponding varinfo.
From [Db]
Functional dependencies between function inputs and function outputs.
Frontc
Signals that we are in MS VC mode
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.
Function_Froms
Datastructures and common operations for the results of the From plugin.
Functions [Globals]
Functions.
Fundec [Cil_datatype]
Funspec [Cil_datatype]

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]
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.

H
Hashconsing_tbl [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.
Hptset [Kernel_function]
Set of kernel functions.
Hptset
Sets over ordered types.
Hptset [Cil_datatype.Varinfo]
Hptset [Cil_datatype.Stmt]
Hptset [Base]

I
IH [Rmciltmps]
IH [Reachingdefs]
IOS [Reachingdefs]
IS [Rmciltmps]
Icon [Gtk_helper]
Some generic icon management tools.
Identified_predicate [Cil_datatype]
Identified_term [Cil_datatype]
Impact [Db]
Impact analysis.
IndexedVal [Parameter_sig.Builder]
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_Interv
Intervals of integers.
Int_Interv_Map
Undocumented.
Int_Intervals [Lattice_Interval_Set]
Int_hashtbl [State_builder]
Int_ref [State_builder]
Build a reference on an integer.
Integer
Extension of Big_int compatible with Zarith.
Interp [Db.Properties]
Interpretation of logic terms.
Ival
Arithmetic lattices.

J
Journal [Kernel]
Kernel for journalization.
Journal
Journalization of functions.

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_debug_level [Cmdline]
Kernel_function
Operations to get info from a kernel function.
Kernel_log [Cmdline]
Kernel_verbose_level [Cmdline]
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
L [Reachingdefs]
L [Liveness]
LBase [Lmap_sig]
LOffset [Lmap_bitwise.Location_map_bitwise]
Label [Cil_datatype]
Lattice_Interval_Set
Sets of disjoint intervals with a lattice structure.
Lattice_type
Lattice signatures.
Launcher
The Frama-C launcher.
Lemmas [Logic_env]
Lenv [Logic_typing]
Local logic environment
Lexerhack
Lexpr [Cil_datatype]
LibEntry [Kernel]
Behavior of option "-lib-entry".
List [Gtk_helper.Custom]
List [Datatype]
List_ref [State_builder]
Build a reference on a list.
List_with_collections [Datatype]
LiveFlow [Liveness]
Liveness
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"
LoadScript [Kernel]
Behavior of option "-load-script"
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 varids and offsets in bits.
Location_Bytes [Locations]
Association between varids 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 contructors 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
Undocumented.
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.
LvExpHash [Availexpslv]
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".
Main [Db]
Frama-C main interface.
MainFunction [Kernel]
Behavior of option "-main".
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_bitwise]
Make [Offsetmap]
Make [Map_Lattice]
Make [Logic_typing]
Make [Int_Interv_Map]
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.
MakeBig [Buckx]
Make_Asymmetric [Binary_cache]
Make_Binary [Binary_cache]
Make_Hashconsed_Lattice_Set [Abstract_interp]
See e.g.
Make_Het1_1_4 [Binary_cache]
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_Symmetric [Binary_cache]
Make_Symmetric_Binary [Binary_cache]
Make_Table [Kernel_function]
Hashtable indexed by kernel functions and dealing with project.
Make_bitwise [Lmap_bitwise]
Make_ordered [Hook]
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]
Acces to slicing results.
Memory [Function_Froms]
Menu_manager
Handle the menubar and the toolbar.
Mergecil
Merge a number of CIL files
Messages
Stored messages.
Model [Cvalue]
Memories.
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
Undocumented.
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.Files]
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_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]
Syntaxic postdominators plugin.
PostdominatorsTypes [Db]
Declarations common to the various postdominators-computing modules
PostdominatorsValue [Db]
Postdominators using value analysis results.
Predicate_named [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"
PrintLib [Kernel]
Behavior of option "-print-lib-path"
PrintPluginPath [Kernel]
Behavior of option "-print-plugin-path"
PrintShare [Kernel]
Behavior of option "-print-share-path"
PrintVersion [Kernel]
Behavior of option "-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_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
RD [Rmciltmps]
RD [Reachingdefs]
Rangemap
Association tables over ordered types.
ReachingDef [Reachingdefs]
Reachingdefs
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.
Report [Db]
Dump Properties-Status consolidation tree.
Request [Db.Slicing]
Requests for slicing jobs.
Reverse_binding [Journal]
Rmciltmps
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.
Semantic_Callgraph [Db]
Callgraph computed by value analysis.
Serializable_undefined [Datatype]
Same as Datatype.Undefined, but the type is supposed to be marshalable by the standard OCaml way (in particular, no hash-consing or projects inside the type).
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_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_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 export: 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 [Reachingdefs.ReachingDef]
StmtStartData [Liveness.LiveFlow]
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.
StmtStartData [Availexpslv.AvailableExps]
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]
StringHashtbl [Parameter_sig.Builder]
StringList [Parameter_sig.Builder]
StringList [Dynamic.Parameter]
List of string parameters.
StringSet [Parameter_sig.Builder]
StringSet [Dynamic.Parameter]
Set of string parameters.
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"
Syntactic_Callgraph [Db]
Interface for the syntactic_callgraph plugin.
Sysutil
System utilities (filename management, etc).

T
TP [Service_graph.Make]
Table [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]
Toolbox
GUI Toolbox.
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.
Trace
Translate_lightweight
Annotate files interpreting lightweight annotations.
Tree [Gtk_helper.Custom]
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.
TypeCheck [Kernel]
Behavior of option "-typecheck"
Typed_parameter
Parameter settable through a command line option.
Typeinfo [Cil_datatype]

U
UD [Rmciltmps]
UD [Reachingdefs]
UD [Liveness]
Undefined [Datatype]
Each values in these modules are undefined.
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_nums
Extends Unmarshal to deal with the data types of the Nums library.
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"
Usedef
compute use/def information
Users [Db]
Functions used by another function.
Utf8_logic
UTF-8 string for logic symbols.

V
V [Cvalue]
Values.
VS [Liveness]
VS [Usedef]
V_Offsetmap [Cvalue]
Memory slices.
V_Or_Uninitialized [Cvalue]
Values with 'undefined' and 'escaping addresses' flags.
Value [Db]
The Value analysis itself.
Value_Message_Callback [Value_messages]
Value_messages
Value_types
Declarations that are useful for plugins written on top of the results of Value.
Varinfo [Cil_datatype]
Varinfo_Id [Cil_datatype]
Varinfo_hashtbl [Cil_state_builder]
Vars [Globals]
Globals variables.
Vector
Extensible Arrays
Verbose [Plugin.S]
Verbose_level [Cmdline]
Vid [Cil_const]
Visitor
Frama-C visitors dealing with projects.

W
WarnDecimalFloat [Kernel]
Behavior of option "-warn-decimal-float"
WarnUndeclared [Kernel]
Behavior of option "-warn-call-to-undeclared"
Warning_manager
Handle Frama-C warnings in the GUI.
Weak [Datatype]
Weak_hashtbl [State_builder]
Build a weak hashtbl over a datatype Data from a reference implementation W.
Wide_string [Cil_datatype]
Widen_Hints [Ival]
Widen_type
Widening hints for the Value Analysis datastructures.
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.

Z
Zero [Parameter_sig.Builder]
Zero_ref [State_builder]
Build a reference on an integer, initialized with 0.
Zone [Locations]
Association between varids and ranges of bits.