A | |
AbsoluteValidRange [Kernel] | Behavior of option "-absolute-valid-range" |
Abstract [Type] | Apply this functor to access to the abstract type of the given name. |
Abstract_interp | Functors for generic lattices implementations. |
Action [Parameter_sig.Builder] | |
AfterTable_By_Callstack [Db.Value] | Table containing the state of the value analysis after the evaluation of each reachable and evaluable statement. |
AggressiveMerging [Kernel] | Behavior of option "-aggressive-merging" |
Alarms | Alarms Database. |
Allocates | Generation of default |
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 |
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 | |
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 |
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 [Transitioning] | See above documentation for |
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 | |
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 |
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 | 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] | |
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" |
CppGnuLike [Kernel] | Behavior of option "-cpp-frama-c-compliant" |
Cprint | Printers for the Cabs AST |
CurrentLoc [Cil_const] | forward reference to current location (see |
CurrentLoc [Cil] | A reference to the current location. |
D | |
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 |
Dgraph_helper | Create a new window displaying a graph. |
Dir_name [Parameter_sig.Specific_dir] | Option |
DoCollapseCallCast [Kernel] | Behavior of option "-collapse-call-cast". |
Dominators | Computation of dominators. |
Dot [State_dependency_graph] | |
Dynamic | Value accesses through dynamic typing. |
Dynlink [Transitioning] | 4.08 |
E | |
Edge [Interpreted_automata] | |
Eid [Cil] | |
Emitted_status [Property_status] | |
Emitter | Emitter. |
Empty_string [Parameter_sig.Builder] | |
Enable [Kernel.Journal] | Behavior of option "-journal-enable" |
Enuminfo [Cil_datatype] | |
Enumitem [Cil_datatype] | |
Enums [Kernel] | Behavior of option "-enums" |
Errorloc | The module stores the current file,line, and working directory in a hidden internal state, modified by the three following functions. |
Escape | OCaml types used to represent wide characters and strings |
Exn_flow | Manages information related to possible exceptions thrown by each function in the AST. |
Exp [Cil_datatype] | Note that the equality is based on eid. |
ExpStructEq [Cil_datatype] | |
Exp_hashtbl [Cil_state_builder] | |
Extlib | Useful operations. |
F | |
F [Fval] | |
F [Filter] | Given a module that match the module type described above,
|
FCBuffer | Extensible buffers. |
FCHashtbl | Extension of OCaml's |
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 |
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 | Functions manipulating filepaths. |
Filepath [Datatype] | Type-safe strings representing normalized filepaths. |
Files [Kernel] | Analyzed files |
Filetree | The tree containing the list of modules and functions together with dynamic columns |
Filled_string_set [Parameter_sig.Builder] | |
Filter | |
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 [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 |
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" |
Global [Cil_datatype] | |
Global_annotation [Cil_datatype] | |
Globals | Operations on globals. |
Group [Cmdline] | Group of command line options. |
Gtk_compat | |
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
|
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 |
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 | |
Inputs [Db] | State_builder.of read inputs. |
Instr [Cil_datatype] | |
Int [Parameter_sig.Builder] | |
Int [Dynamic.Parameter] | Integer parameters. |
Int [Datatype] | |
Int [Abstract_interp] | |
Int32 [Datatype] | |
Int64 [Datatype] | |
Int_Base | Big integers with an additional top element. |
Int_Intervals | Sets of intervals with a lattice structure. |
Int_Intervals_sig | Sets of intervals with a lattice structure. |
Int_hashtbl [State_builder] | |
Int_ref [State_builder] | Build a reference on an integer. |
Integer | Extension of |
Integer [Datatype] | |
Interp [Db.Properties] | Interpretation of logic terms. |
Interpreted_automata | |
InvalidBool [Kernel] | Behavior of option "-warn-invalid-bool" |
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 |
|
K | |
KeepSwitch [Kernel] | Behavior of option "-keep-switch" |
Keep_unused_specified_functions [Kernel] | Behavior of option "-keep-unused-specified-function". |
Kernel | Provided services for kernel developers. |
Kernel_function | Operations to get info from a kernel function. |
Kernel_function_hashtbl [Cil_state_builder] | |
Kernel_function_map [Parameter_sig.Builder] | As for Kernel_function_set, by default keys can only be defined functions. |
Kernel_function_multiple_map [Parameter_sig.Builder] | As for Kernel_function_set, by default keys can only be defined functions. |
Kernel_function_set [Parameter_sig.Builder] | |
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" |
Leftistheap | Leftist heaps. |
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 |
List [Transitioning] | |
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_interp | All the interesting functions of this module are exported through
|
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 |
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 [Leftistheap] | |
Make [Indexer] | |
Make [Hptset] | |
Make [Hptmap] | |
Make [Hook] | Make a new empty hook from |
Make [Float_interval] | |
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] | 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 |
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 |
Map [Datatype] | |
Map [Datatype.S_with_collections] | |
Map_lattice | Maps equipped with a lattice structure. |
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] | |
Normalized [Filepath] | The |
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_lattice_with_isotropy | Type of the arguments of functor |
Offsetmap_sig | Signature for |
Oneret | |
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 | |
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. |
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 |
Qstack | Mutable stack in which it is possible to add data at the end (like a queue) and to handle non top elements. |
Quadruple [Datatype] | |
Quadruple_with_collections [Datatype] | |
Queue [State_builder] | |
Queue [Datatype] | |
Quiet [Kernel] | Behavior of option "-quiet" |
R | |
Rangemap | Association tables over ordered types. |
ReadAnnot [Kernel] | Behavior of option "-read-annot" |
Record_From_Callbacks [Db.From] | |
Record_Value_After_Callbacks [Db.Value] | |
Record_Value_Callbacks [Db.Value] | |
Record_Value_Superposition_Callbacks [Db.Value] | |
Recursive [Structural_descr] | Use this module for handling a (possibly recursive) structural descriptor
|
Ref [State_builder] | |
Ref [Datatype] | |
Register [State_builder] |
|
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" |
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 | |
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 |
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 [Datatype] | |
Set [Datatype.S_with_collections] | |
SetLattice [Base] | |
Set_project_as_default [Kernel] | Undocumented. |
Set_ref [State_builder] | |
Shape [Hptmap] | This functor exports the shape of the maps indexed by keys |
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] | |
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. |
Sparecode [Db] | Interface for the unused code detection. |
SpecialFloat [Kernel] | Behavior of option "-warn-special-float" |
Special_hooks | Nothing is exported: just register some special hooks for Frama-C. |
Stack [Transitioning] | |
StartData [Dataflow2] | This module can be used to instantiate the |
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
|
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 [Transitioning] | In OCaml 4.03, many functions |
String [Parameter_sig.Builder] | |
String [Dynamic.Parameter] | String parameters. |
String [Datatype] | |
StringList [Dynamic.Parameter] | List of string parameters. |
StringSet [Dynamic.Parameter] | Set of string parameters. |
String_list [Parameter_sig.Builder] | |
String_map [Parameter_sig.Builder] | |
String_multiple_map [Parameter_sig.Builder] | |
String_set [Parameter_sig.Builder] | |
String_tbl [Type] | Heterogeneous tables indexed by string. |
Structural_descr | Internal representations of OCaml type as first class values. |
SymbolicPath [Kernel] | Behavior of option "-add-symbolic-path" |
Symmetric_Binary [Binary_cache] | |
Symmetric_Binary_Predicate [Binary_cache] | |
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 |
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 |
Unmarshal_z | |
UnrollUnnatural [Interpreted_automata] | |
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" |
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. |
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 |
Wfile | |
Wide_string [Cil_datatype] | |
Widen_Hints [Ival] | |
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
|
Wpalette | |
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 |
|
Z | |
Zero [Parameter_sig.Builder] | |
Zero_ref [State_builder] | Build a reference on an integer, initialized with |
Zone [Locations] | Association between bases and ranges of bits. |