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