A | |
AbsoluteValidRange [Kernel] | Behavior of option "-absolute-valid-range" |
Abstract [Type] | Apply this functor to access to the abstract type of the given name. |
Abstract_interp | Functors for generic lattices implementations. |
Acsl_extension | ACSL extensions registration module |
Action [Parameter_sig.Builder] | |
AfterTable_By_Callstack [Db.Value] | Table containing the state of the value analysis after the evaluation of each reachable and evaluable statement. |
AggressiveMerging [Kernel] | Behavior of option "-aggressive-merging" |
Alarms | Alarms Database. |
Allocates | Generation of default |
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] | |
AuditCheck [Kernel] | Behavior of option "-audit-check" |
AuditPrepare [Kernel] | Behavior of option "-audit-prepare" |
AutoLoadPlugins [Kernel] | Behavior of option "-autoload-plugins" |
AutocompleteHelp [Kernel] | Behavior of option "-autocomplete" |
Automaton [Interpreted_automata] | Datatype for automata |
Axiomatics [Logic_env] | |
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_builtins] | 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 [Datatype] | |
Check [Kernel] | Behavior of option "-check" |
Cil | CIL main API. |
Cil_builtins | |
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_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] | |
Contract_special_float | |
Copy [Kernel] | Behavior of option "-copy" |
Counter [State_builder] | Creates a projectified counter. |
Cparser | |
CppCommand [Kernel] | Behavior of option "-cpp-command" |
CppExtraArgs [Kernel] | Behavior of option "-cpp-extra-args" |
CppExtraArgsPerFile [Kernel] | Behavior of option "-cpp-extra-args-per-file" |
CppGnuLike [Kernel] | Behavior of option "-cpp-frama-c-compliant" |
Cprint | Printers for the Cabs AST |
CurrentLoc [Cil_const] | forward reference to current location (see |
CurrentLoc [Cil] | A reference to the current location. |
D | |
Dataflow [Interpreted_automata] | Builds a simple dataflow analysis over an input domain. |
Dataflow2 | Implementation of data flow analyses over user-supplied domains. |
Dataflows | Implementation of data flow analyses over user-supplied domains. |
Datatype [State_builder.S] | |
Datatype [Service_graph.S.Service_graph] | |
Datatype [Project] | |
Datatype [Datatype.Caml_weak_hashtbl] | |
Datatype | A datatype provides useful values for types. |
Db | Database in which static plugins are registered. |
Debug [Plugin.S_no_log] | |
Descr | Type descriptor for safe unmarshalling. |
Description | Describe items of Source and Properties. |
Design | The extensible GUI. |
Destructors | retrieve local variables with |
Dgraph_helper | Create a new window displaying a graph. |
DoCollapseCallCast [Kernel] | Behavior of option "-collapse-call-cast". |
Dominators | Computation of dominators. |
Dot [State_dependency_graph] | |
Dotgraph | Helper for Printing Dot-graphs. |
Dump_config | |
Dynamic | Value accesses through dynamic typing. |
E | |
Edge [Interpreted_automata] | |
Eid [Cil_const] | |
Emitted_status [Property_status] | |
Emitter | Emitter. |
Empty_string [Parameter_sig.Builder] | |
Enable [Kernel.Journal] | Behavior of option "-journal-enable" |
Enuminfo [Cil_datatype] | |
Enumitem [Cil_datatype] | |
Enums [Kernel] | Behavior of option "-enums" |
Errorloc | The module stores the current file,line, and working directory in a hidden internal state, modified by the three following functions. |
Escape | OCaml types used to represent wide characters and strings |
Eva_lattice_type | Lattice signatures using the Bottom type: these lattices do not include a bottom element, and return `Bottom instead when needed. |
Exn_flow | Manages information related to possible exceptions thrown by each function in the AST. |
Exp [Cil_datatype] | Note that the equality is based on eid. |
ExpStructEq [Cil_datatype] | |
Exp_hashtbl [Cil_state_builder] | |
Extlib | Useful operations. |
F | |
F [Fval] | |
F [Filter] | Given a module that match the module type described above,
|
FCHashtbl | Extension of OCaml's |
False [Parameter_sig.Builder] | |
False_ref [State_builder] | Build a reference on a boolean, initialized with |
Fc_Filepath [Parameter_sig.Builder] | |
Fc_config | Information about version of Frama-C. |
Fc_float | Implementation of floating-point values of different precision, using the standard ocaml floating-point numbers in double precision. |
Feedback [Property_status] | Lighter version than Consolidation |
Feedback [Design] | Bullets in left-margins |
Fieldinfo [Cil_datatype] | |
File | Frama-c preprocessing and Cil AST initialization. |
File [Cil_datatype] | |
FileIndex [Globals] | Globals associated to filename. |
File_manager | Nothing exported. |
Filecheck | This file performs various consistency checks over a cil file. |
Filepath [Parameter_sig.Builder] | |
Filepath | Functions manipulating filepaths. |
Filepath [Dynamic.Parameter] | Filepath parameters. |
Filepath [Datatype] | Type-safe strings representing normalized filepaths. |
Filepath_list [Parameter_sig.Builder] | |
Filepath_map [Parameter_sig.Builder] | |
Files [Kernel] | Analyzed files |
Filetree | The tree containing the list of modules and functions together with dynamic columns |
Filled_string_set [Parameter_sig.Builder] | |
Filter | |
Float [Datatype] | |
FloatHex [Kernel] | Behavior of option "-float-hex" |
FloatNormal [Kernel] | Behavior of option "-float-normal" |
FloatRelative [Kernel] | Behavior of option "-float-relative" |
Float_interval | Builds a semantics of floating-point intervals for different precisions, from a module providing the floating-point numbers used for the bounds of the intervals. |
Float_interval_sig | Signature for the floating-point interval semantics. |
Float_ref [State_builder] | Build a reference on a float. |
Float_sig | Interface of floating-point numbers of different precisions. |
Floating_point | Floating-point operations. |
Fold [Visitor_behavior] | Fold operations on table of a given type of AST elements. |
Fold [Hook] | |
Fold_ordered [Hook] | |
Formatter [Datatype] | |
Forwards [Dataflow2] | |
FramaCStdLib [Kernel] | Behavior of option "-frama-c-stdlib" |
Frama_c_builtins [Cil_builtins] | 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" |
Get [Visitor_behavior] | Get operations on behaviors, allows to get the representative of an AST element in the current state of the visitor. |
Get_orig [Visitor_behavior] | Get operations on behaviors, allows to get the original representative of an element of the new AST in the curent state of the visitor. |
Ghost_accesses | Checks that memory accesses are well-typed in the sense of the |
Ghost_cfg | Checks that normal cfg is not altered by ghost statements. |
Global [Cil_datatype] | |
Global_annotation [Cil_datatype] | |
Globals | Operations on globals. |
Group [Cmdline] | Group of command line options. |
Gtk_compat | |
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_interval | Integer intervals with congruence. |
Int_ref [State_builder] | Build a reference on an integer. |
Int_set | Small sets of integers. |
Int_val | Integer values abstractions: an abstraction represents a set of integers. |
Integer | Extension of |
Integer [Datatype] | |
Interp [Db.Properties] | Interpretation of logic terms. |
Interpreted_automata | |
InvalidBool [Kernel] | Behavior of option "-warn-invalid-bool" |
InvalidPointer [Kernel] | Behavior of option "-warn-invalid-pointer" |
Iter [Visitor_behavior] | Iter operations on the table of a given type of AST elements. |
Ival | Arithmetic lattices. |
J | |
Journal [Kernel] | Kernel for journalization. |
Journal | Journalization of functions. |
Json | Json Library |
JsonCompilationDatabase [Kernel] | Behavior of option "-json-compilation-database" |
Json_compilation_database |
|
K | |
KeepSwitch [Kernel] | Behavior of option "-keep-switch" |
Keep_unused_specified_functions [Kernel] | Behavior of option "-keep-unused-specified-functions". |
Keep_unused_types [Kernel] | Behavior of option "-keep-unused-types". |
Kernel | Provided services for kernel developers. |
Kernel_function | Operations to get info from a kernel function. |
Kernel_function_hashtbl [Cil_state_builder] | |
Kernel_function_map [Parameter_sig.Builder] | As for Kernel_function_set, by default keys can only be defined functions. |
Kernel_function_multiple_map [Parameter_sig.Builder] | As for Kernel_function_set, by default keys can only be defined functions. |
Kernel_function_set [Parameter_sig.Builder] | |
Kernel_function_set [Kernel] | |
Key [Datatype.Hashtbl] | Datatype for the keys of the hashtbl. |
Key [Datatype.Map] | Datatype for the keys of the map. |
Kf [Cil_datatype] | |
Kinstr [Cil_datatype] | |
Kinstr_hashtbl [Cil_state_builder] | |
L | |
LOffset [Lmap_bitwise.Location_map_bitwise] | |
Label [Cil_datatype] | |
Lattice_messages | Message and logging facility for abstract lattices. |
Lattice_type | Lattice signatures. |
Launcher | The Frama-C launcher. |
LeftShiftNegative [Kernel] | Behavior of option "-warn-left-shift-negative" |
LegacyNames [Property] | |
Lemmas [Logic_env] | |
Lenv [Logic_typing] | Local logic environment |
Lexerhack | |
Lexpr [Cil_datatype] | Beware: no pretty-printer is available. |
LibEntry [Kernel] | Behavior of option "-lib-entry". |
LinkPrinter [Gui_printers] | Special pretty-printer that outputs tags |
List [Datatype] | |
List_ref [State_builder] | Build a reference on a list. |
List_with_collections [Datatype] | |
Lmap | Maps from bases to memory maps. |
Lmap_bitwise | Functors making map indexed by zone. |
Lmap_sig | Signature for maps from bases to memory maps. |
LoadModule [Kernel] | Behavior of option "-load-module" |
LoadState [Kernel] | Behavior of option "-load" |
Localisation [Cil_datatype] | |
Localizable [Printer_tag] | |
Location [Locations] | |
Location [Cil_datatype] | Cil locations. |
LocationLattice [Origin] | Lattice of source locations. |
Location_Bits [Locations] | Association between bases and offsets in bits. |
Location_Bytes [Locations] | Association between bases and offsets in byte. |
Locations | Memory locations. |
Locs [Pretty_source] | |
Log | Logging Services for Frama-C Kernel and Plugins. |
Logic [Db.Value] | Evaluation of logic terms and predicates |
Logic_builtin | |
Logic_builtin_used [Logic_env] | logic function/predicates that are effectively used in current project. |
Logic_const | Smart constructors for logic annotations. |
Logic_constant [Cil_datatype] | |
Logic_ctor_info [Logic_env] | |
Logic_ctor_info [Cil_datatype] | |
Logic_env | Global Logic Environment |
Logic_info [Logic_env] | Global Tables |
Logic_info [Cil_datatype] | |
Logic_info_structural [Cil_datatype] | Logic_info with structural comparison: name of the symbol, type of arguments Note that polymorphism is ignored, in the sense that two symbols with the same name and profile except for the name of their type variables will compare unequal. |
Logic_interp | All the interesting functions of this module are exported through
|
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-operators: 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 [Indexer] | |
Make [Hptset] | |
Make [Hptmap] | |
Make [Hook] | Make a new empty hook from |
Make [Float_interval] | |
Make [FCHashtbl] | |
Make [Datatype.Polymorphic4] | |
Make [Datatype.Polymorphic3] | |
Make [Datatype.Polymorphic2] | |
Make [Datatype.Polymorphic] | Create a datatype for a monomorphic instance of the polymorphic type. |
Make [Datatype] | Generic datatype builder. |
Make [Datatype.Hashtbl] | Build a datatype of the hashtbl according to the datatype of values in the hashtbl. |
Make [Datatype.Map] | Build a datatype of the map according to the datatype of values in the map. |
Make_Datatype [Bottom] | Datatype constructor. |
Make_Hashconsed_Lattice_Set [Abstract_interp] | See e.g. |
Make_LOffset [Lmap] | |
Make_Lattice_Base [Abstract_interp] | |
Make_Lattice_Product [Abstract_interp] | If |
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. |
Markdown | Markdown Document Structured representation of Markdown content. |
Memo [Visitor_behavior] | Memo operations on behaviors, allows to get a binding in the new project for the given AST element, creating one if it does not already exists. |
Menu_manager | Handle the menubar and the toolbar. |
Mergecil | Merge a number of CIL files |
Messages | Stored messages for persistence between sessions. |
Model_info [Logic_env] | |
Model_info [Cil_datatype] | |
N | |
Name [Kernel.Journal] | Behavior of option "-journal-name" |
Names [Property] | |
Nativeint [Datatype] | |
Node [Dotgraph] | Lazily associates a node to any element. |
Normalized [Filepath] | The |
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_by_function [Property] | Datatype with alternative ordering, where properties are ordered according the following criteria: 1. |
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. |
Permissive [Kernel] | Behavior of option "-permissive" |
Plugin | Special signature for Kernel services, whose messages are handled in an ad'hoc manner. |
PointerDowncast [Kernel] | Behavior of option "-warn-pointer-downcast" |
Poly_array [Datatype] | |
Poly_list [Datatype] | |
Poly_option [Datatype] | |
Poly_pair [Datatype] | |
Poly_queue [Datatype] | |
Poly_ref [Datatype] | |
Polymorphic [Type] | Generic implementation of polymorphic type value. |
Polymorphic [Datatype] | Functor for polymorphic types with only 1 type variable. |
Polymorphic2 [Type] | Generic implementation of polymorphic type value with two type variables. |
Polymorphic2 [Datatype] | Functor for polymorphic types with 2 type variables. |
Polymorphic3 [Type] | Generic implementation of polymorphic type value with three type variables. |
Polymorphic3 [Datatype] | Functor for polymorphic types with 3 type variables. |
Polymorphic4 [Type] | Generic implementation of polymorphic type value with four type variables. |
Polymorphic4 [Datatype] | Functor for polymorphic types with 4 type variables. |
Position [Cil_datatype] | Single position in a file. |
Postdominators [Db] | Syntactic postdominators plugin. |
PostdominatorsTypes [Db] | Declarations common to the various postdominators-computing modules |
PostdominatorsValue [Db] | Postdominators using value analysis results. |
Predicate [Cil_datatype] | |
PreprocessAnnot [Kernel] | Behavior of option "-pp-annot" |
Pretty_source | Utilities to pretty print source with located elements in a Gtk TextBuffer. |
Pretty_utils | Pretty-printer utilities. |
PrintCode [Kernel] | Behavior of option "-print" |
PrintComments [Kernel] | Behavior of option "-keep-comments" |
PrintConfig [Kernel] | Behavior of option "-print-config" |
PrintConfigJson [Kernel] | Behavior of option "-print-config-json" |
PrintCppCommands [Kernel] | Behavior of option "-print-cpp-commands" |
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 | |
Qstack | Mutable stack in which it is possible to add data at the end (like a queue) and to handle non top elements. |
Quadruple [Datatype] | |
Quadruple_with_collections [Datatype] | |
Queue [State_builder] | |
Queue [Datatype] | |
Quiet [Kernel] | Behavior of option "-quiet" |
R | |
Rangemap | Association tables over ordered types. |
ReadAnnot [Kernel] | Behavior of option "-read-annot" |
Record [Dotgraph] | Complex node layout. |
Record_From_Callbacks [Db.From] | |
Record_Value_After_Callbacks [Db.Value] | |
Record_Value_Callbacks [Db.Value] | |
Record_Value_Superposition_Callbacks [Db.Value] | |
Recursive [Structural_descr] | Use this module for handling a (possibly recursive) structural descriptor
|
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" |
Reset [Visitor_behavior] | Reset operations on behaviors, allows to reset the tables associated to a given kind of AST elements. |
Reverse_binding [Journal] | |
Rgmap | Associative maps for _ranges_ to _values_ with overlapping. |
Rich_text | Text with Tags |
RightShiftNegative [Kernel] | Behavior of option "-warn-right-shift-negative" |
Rmtmps | |
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 [Visitor_behavior] | Set operations on behaviors, allows to change the representative of a given AST element in the current state of the visitor. |
Set [Datatype] | |
Set [Datatype.S_with_collections] | |
SetLattice [Base] | |
Set_orig [Visitor_behavior] | Set operations on behaviors related to original representatives, allows to change the reference of an element of the new AST in the current state of the visitor. |
Set_project_as_default [Kernel] | Undocumented. |
Set_ref [State_builder] | |
Shape [Hptmap] | This functor exports the shape of the maps indexed by keys |
Share [Plugin.S_no_log] | Handle the specific `share' directory of the plug-in. |
SharedCounter [State_builder] | Creates a counter that is shared among all projects, but which is marshalling-compliant. |
Sid [Cil_const] | |
SignedDowncast [Kernel] | Behavior of option "-warn-signed-downcast" |
SignedOverflow [Kernel] | Behavior of option "-warn-signed-overflow" |
Simple_backward [Dataflows] | |
Simple_forward [Dataflows] | |
SimplifyCfg [Kernel] | Behavior of option "-simplify-cfg" |
SimplifyTrivialLoops [Kernel] | Behavior of option "-simplify-trivial-loops". |
Source_manager | The source viewer multi-tabs widget window. |
Source_viewer | The Frama-C source viewer. |
SpecialFloat [Kernel] | Behavior of option "-warn-special-float" |
Special_hooks | Nothing is exported: just register some special hooks for Frama-C. |
StartData [Dataflow2] | This module can be used to instantiate the |
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. |
Stmt [Cil_datatype] | |
StmtStartData [Dataflow2.BackwardsTransfer] | For each block id, the data at the start. |
StmtStartData [Dataflow2.ForwardsTransfer] | For each statement id, the data at the start. |
Stmt_Id [Cil_datatype] | |
Stmt_hashtbl [Cil_state_builder] | |
Stmt_set_ref [Cil_state_builder] | |
Stmts_graph | Statements graph. |
String [Parameter_sig.Builder] | |
String [Dynamic.Parameter] | String parameters. |
String [Datatype] | |
StringList [Dynamic.Parameter] | List of string parameters. |
StringSet [Dynamic.Parameter] | Set of string parameters. |
String_list [Parameter_sig.Builder] | |
String_map [Parameter_sig.Builder] | |
String_multiple_map [Parameter_sig.Builder] | |
String_set [Parameter_sig.Builder] | |
String_tbl [Type] | Heterogeneous tables indexed by string. |
Structural_descr | Internal representations of OCaml type as first class values. |
Substitute_const_globals | A visitor that substitutes globals, defined with the attribute 'const', with respective initializers. |
SymbolicPath [Kernel] | Behavior of option "-add-symbolic-path" |
Symmetric_Binary [Binary_cache] | |
Symmetric_Binary_Predicate [Binary_cache] | |
Syntactic_scope [Cil_datatype] | |
Syntactic_search [Globals] | |
T | |
TP [Service_graph.S] | |
Table_By_Callstack [Db.Value] | Table containing the results of the value analysis, ie. |
Task | High Level Interface to Command. |
Term [Cil_datatype] | |
Term_lhost [Cil_datatype] | |
Term_lval [Cil_datatype] | |
Term_offset [Cil_datatype] | |
Time [Kernel] | Behavior of option "-time" |
To_zone [Logic_interp] | |
To_zone [Db.Properties.Interp] | |
Top [Bottom] | Lattices in which both top and bottom are managed separately |
Toplevel [Db] | |
Toplevel_predicate [Cil_datatype] | |
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" |
Unset [Visitor_behavior] | Operations to remove the entry associated to a given AST element in the current state of the visitor. |
Unset_orig [Visitor_behavior] | Operations to remove the entry associated to a given element of the new AST in the current state of the visitor. |
UnsignedDowncast [Kernel] | Behavior of option "-warn-unsigned-downcast" |
UnsignedOverflow [Kernel] | Behavior of option "-warn-unsigned-overflow" |
UnspecifiedAccess [Kernel] | Behavior of option "-unspecified-access" |
UntypedFiles [Ast] | |
Usable_emitter [Emitter] | Usable emitters are the ones which can really emit something. |
UseUnicode [Kernel] | Behavior of option "-unicode" |
Utf8_logic | UTF-8 string for logic symbols. |
UtilsFilepath [Cil_datatype] | |
V | |
Validity [Base] | |
Value [Db] | The Value analysis itself. |
Varinfo [Cil_datatype] | |
Varinfo_Id [Cil_datatype] | |
Varinfo_hashtbl [Cil_state_builder] | |
Vars [Globals] | Globals variables. |
Vector | Extensible Arrays |
Verbose [Plugin.S_no_log] | |
Version [Interpreted_automata.UnrollUnnatural] | |
Vertex [Interpreted_automata] | Datatype for vertices |
Vertex_Set [Interpreted_automata.UnrollUnnatural] | |
Vid [Cil_const] | |
Visitor | Frama-C visitors dealing with projects. |
Visitor_behavior | Operations on visitor behaviors. |
W | |
WTO [Wto_statement] | The datatype for statement WTOs |
WTO [Interpreted_automata.UnrollUnnatural] | |
WTO [Interpreted_automata] | |
WTOIndex [Wto_statement] | Datatype for wto_index |
WTOIndex [Interpreted_automata] | Datatype for wto_index |
WarnDecimalFloat [Kernel] | |
Warning_manager | Handle Frama-C warnings in the GUI. |
Wbox | Box Layouts. |
Weak [Datatype] | |
Weak_hashtbl [State_builder] | Build a weak hashtbl over a datatype |
Wfile | |
Wide_string [Cil_datatype] | |
Widen_Hints [Ival] | |
Widen_Hints [Int_val] | |
Widen_Hints [Float_sig.S] | |
Widget | Simple Widgets |
WithOutput [Parameter_sig.Builder] | |
With_Cardinality [Map_lattice.Make_MapSet_Lattice] | |
With_Cardinality [Map_lattice.Make_Map_Lattice] | Adds cardinality functions for maps, according to a notion of cardinality on the values. |
With_collections [Datatype] | Add sets, maps and hashtables modules to an existing datatype, provided the
|
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. |