Index of modules

A
AbsoluteValidRange [Kernel]

Behavior of option "-absolute-valid-range"

Abstract [Type]

Apply this functor to access to the abstract type of the given name.

Abstract_interp

Functors for generic lattices implementations.

Action [Parameter_sig.Builder]
AfterTable_By_Callstack [Db.Value]

Table containing the state of the value analysis after the evaluation of each reachable and evaluable statement.

AggressiveMerging [Kernel]

Behavior of option "-aggressive-merging"

Alarms

Alarms Database.

Allocates

Generation of default allocates \nothing clauses.

AllowDuplication [Kernel]

Behavior of option "-allow-duplication".

Alpha

Alpha conversion.

Analyses_manager

Nothing exported.

Annotations

Annotations in the AST.

Arity_One [Binary_cache]
Arity_Three [Binary_cache]
Arity_Two [Binary_cache]
Array [State_builder]
Array [Datatype]
Array_with_collections [Datatype]
As_string [Parameter_sig.Collection]

A collection is a standard string parameter

AsmContractsAutoValidate [Kernel]

Behavior of option "-asm-contracts-auto-validate."

AsmContractsGenerate [Kernel]

Behavior of option "-asm-contracts"

Asm_contracts

Code transformation for inferring contracts from information given in GNU's extended assembly syntax.

Ast

Access to the CIL AST which must be used from Frama-C.

Ast_info

AST manipulation utilities.

Attribute [Cil_datatype]
Attributes [State_dependency_graph]
Attributes [Cil_datatype]
AutoLoadPlugins [Kernel]

Behavior of option "-autoload-plugins"

Automaton [Interpreted_automata]

Datatype for automata

B
Backwards [Dataflow2]
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"

Binary_Predicate [Binary_cache]
Binary_cache

Very low-level abstract functorial caches.

Binding [Journal]
Bit_utils

Some bit manipulations.

Bitvector

Bitvectors.

Block [Cil_datatype]
Bool [Parameter_sig.Builder]
Bool [Dynamic.Parameter]

Boolean parameters.

Bool [Datatype]
Bool [Abstract_interp]
Bool_ref [State_builder]

Build a reference on a boolean.

Bottom

Types, monads and utilitary functions for lattices in which the bottom is managed separately from other values.

Bound_Lattice [Bottom]

Bounds a semi-lattice.

Build [Hook]

Make a new empty hook from a given type of parameters.

Build_ordered [Hook]
Builtin_functions [Cil]

A list of the built-in functions for the current compiler (GCC or MSVC, depending on !msvcMode).

Builtin_logic_info [Cil_datatype]
Builtins [Logic_env]
C
C11 [Kernel]

Behavior of option "-c11"

Cabs

Untyped AST.

Cabs2cil

Registers a new hook that will be applied each time a side-effect free expression whose result is unused is dropped.

Cabs_debug
Cabs_file [Cil_datatype]
Cabshelper

Helper functions for Cabs

Cabsvisit
Call_Type_Value_Callbacks [Db.Value]

Actions to perform at each treatment of a "call" statement.

Call_Value_Callbacks [Db.Value]

Actions to perform at each treatment of a "call" statement.

Callwise [Db.From]
Caml_weak_hashtbl [State_builder]

Build a weak hashtbl over a datatype Data by using Weak.Make provided by the OCaml standard library.

Caml_weak_hashtbl [Datatype]
Category [Parameter_sig.Collection]

Categories for this collection.

Cfg

Code to compute the control-flow graph of a function or file.

Char [Transitioning]

See above documentation for String

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 Compositional_bool argument of the functor Hptmap.Make.

Compinfo [Cil_datatype]
Compute [Interpreted_automata]

This module defines the previous functions without memoization

Compute_Statement_Callbacks [Db.Value]

Actions to perform whenever a statement is handled.

Config [Plugin.S_no_log]

Handle the specific `config' directory of the plug-in.

Config

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.

ConstReadonly [Kernel]

Global variables with "const" qualifier are constant.

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]

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 Cil.CurrentLoc)

CurrentLoc [Cil]

A reference to the current location.

D
Dataflow

Deprecated: use Dataflows instead.

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

Nothing exported.

Descr

Type descriptor for safe unmarshalling.

Description

Describe items of Source and Properties.

Design

The extensible GUI.

Destructors

retrieve local variables with __fc_destructor attribute and add the appropriate calls to the corresponding destructor function when we exit the scope of the variable.

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

Value accesses through dynamic typing.

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, F.build_cil_file initializes a new project containing the slices

FCBuffer

Extensible buffers.

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

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_ref [State_builder]

Build a reference on a float.

Floating_point

Floating-point operations.

Fold [Hook]
Fold_ordered [Hook]
Formatter [Datatype]
Forwards [Dataflow2]
Forwards [Dataflow]
FramaCStdLib [Kernel]

Behavior of option "-frama-c-stdlib"

Frama_c_builtins [Cil]

This module associates the name of a built-in function that might be used during elaboration with the corresponding varinfo.

Frama_c_init

Setting global, platform-wide settings.

From [Db]

Functional dependencies between function inputs and function outputs.

Frontc

Signals that we are in MS VC mode

Funbehavior [Cil_datatype]
Function [Type]

Instance of Type.Polymorphic2 for functions: same signature than Type.Polymorphic2 with possibility to specify a label for the function parameter.

Function [Datatype]
Function [Ast_info]

Operations on cil function.

Functions [Globals]

Functions.

Fundec [Cil_datatype]
Fundec_set [Parameter_sig.Builder]
Funspec [Cil_datatype]
Fval

Floating-point intervals, used to construct arithmetic lattices.

G
G [State_dependency_graph.S]
G [Interpreted_automata.UnrollUnnatural]
G [Interpreted_automata]
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_form

DEPRECATED.

Gtk_helper

Generic Gtk helpers.

Gui_init

Very early initialization step required by any GUI.

Gui_parameters

GUI as a plug-in.

Gui_printers

Special pretty-printers for the GUI.

H
Hashcons [State_builder]

Hashconsed version of an arbitrary datatype

Hashconsing_tbl [State_builder]

Weak or non-weak hashconsing tables, depending on variable Cmdline.deterministic.

Hashconsing_tbl_not_weak [State_builder]

Hash table for hashconsing, but the internal table is _not_ weak (it is a regular hash table).

Hashconsing_tbl_weak [State_builder]

Weak hashtbl dedicated to hashconsing.

Hashtbl [State_builder]
Hashtbl [Datatype]
Hashtbl [Datatype.S_with_collections]
Help [Plugin.S_no_log]
Help_manager

Nothing exported.

History

Source code navigation history.

Hook

Hook builder.

Hptmap

Efficient maps from hash-consed trees to values, implemented as Patricia trees.

Hptmap_sig

Signature for the Hptmap module

Hptset [Kernel_function]

Set of kernel functions.

Hptset

Sets over ordered types.

Hptset [Cil_datatype.Varinfo]
Hptset [Cil_datatype.Stmt]
Hptset [Base]
I
Icon [Gtk_helper]

Some generic icon management tools.

Identified_predicate [Cil_datatype]
Identified_term [Cil_datatype]
ImplicitFunctionDeclaration [Kernel]

Behavior of option "-implicit-function-declaration"

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 Big_int compatible with Zarith.

Integer [Datatype]
Interp [Db.Properties]

Interpretation of logic terms.

Interpreted_automata
Ival

Arithmetic lattices.

J
Journal [Kernel]

Kernel for journalization.

Journal

Journalization of functions.

Json

Json Library

JsonCompilationDatabase [Kernel]

Behavior of option "-json-compilation-database"

Json_compilation_database

get_flags f returns the preprocessing flags associated to file f in the JSON compilation database (when enabled), or the empty string otherwise.

K
KeepSwitch [Kernel]

Behavior of option "-keep-switch"

Keep_unused_specified_functions [Kernel]

Behavior of option "-keep-unused-specified-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.

Leftistheap

Leftist heaps.

Lemmas [Logic_env]
Lenv [Logic_typing]

Local logic environment

Lexerhack
Lexpr [Cil_datatype]

Beware: no pretty-printer is available.

LibEntry [Kernel]

Behavior of option "-lib-entry".

LinkPrinter [Gui_printers]

Special pretty-printer that outputs tags link:vidN around varinfos, and link:typN around types.

List [Datatype]
List_ref [State_builder]

Build a reference on a list.

List_with_collections [Datatype]
Lmap

Maps from bases to memory maps.

Lmap_bitwise

Functors making map indexed by zone.

Lmap_sig

Signature for maps from bases to memory maps.

LoadModule [Kernel]

Behavior of option "-load-module"

LoadState [Kernel]

Behavior of option "-load"

Localisation [Cil_datatype]
Localizable [Pretty_source]
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 Db.Interp.

Logic_label [Cil_datatype]
Logic_lexer
Logic_parser
Logic_preprocess

adds another pre-processing step in order to expand macros in annotations.

Logic_print

Pretty-printing of a parsed logic tree.

Logic_ptree

logic constants.

Logic_type [Cil_datatype]

Logic_type.

Logic_type_ByName [Cil_datatype]
Logic_type_NoUnroll [Cil_datatype]
Logic_type_info [Logic_env]
Logic_type_info [Cil_datatype]
Logic_typing

Logic typing and logic environment.

Logic_utils

Utilities for ACSL constructs.

Logic_var [Cil_datatype]
LogicalOperators [Kernel]

Behavior of invisible option -keep-logical operator: Tries to avoid converting && and || into conditional statements.

Loop

Operations on (natural) loops.

Lval [Cil_datatype]

Note that the equality is based on eid (for sub-expressions).

LvalStructEq [Cil_datatype]
Lval_hashtbl [Cil_state_builder]
M
M [Locations.Location_Bytes]
MAKE_CUSTOM_LIST [Gtk_helper]

A functor to build custom Gtk lists.

Machdep [Kernel]

Behavior of option "-machdep".

Machdeps

Some predefined Cil_types.mach which specifies machine-dependent data about C programs.

Main [Db]

Frama-C main interface.

MainFunction [Kernel]

Behavior of option "-main".

Make [Wto]

This functor provides the partitioning algorithm constructing a WTO.

Make [State_topological]

Functor providing topological iterators over a graph.

Make [Service_graph]

Generic functor implementing the services algorithm according to a graph implementation.

Make [Rangemap]

Extension of the above signature, with specific functions acting on range of values

Make [Qstack]
Make [Printer_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 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]

Generic datatype builder.

Make [Datatype.Hashtbl]

Build a datatype of the hashtbl according to the datatype of values in the hashtbl.

Make [Datatype.Map]

Build a datatype of the map according to the datatype of values in the map.

Make_Datatype [Bottom]

Datatype constructor.

Make_Hashconsed_Lattice_Set [Abstract_interp]

See e.g.

Make_LOffset [Lmap]
Make_Lattice_Base [Abstract_interp]
Make_Lattice_Product [Abstract_interp]

If C.collapse then L1.bottom,_ = _,L2.bottom = bottom

Make_Lattice_Set [Abstract_interp]
Make_Lattice_Sum [Abstract_interp]
Make_Lattice_UProduct [Abstract_interp]

Uncollapsed product.

Make_MapSet_Lattice [Map_lattice]

Builds a lattice mixing maps and sets, provided that each one has a lattice structure.

Make_Map_Lattice [Map_lattice]

Equips an Hptmap with a lattice structure, provided that the values have a lattice structure.

Make_Narrow [Offsetmap_sig]
Make_Narrow [Lmap_sig]
Make_Table [Kernel_function]

Hashtable indexed by kernel functions and dealing with project.

Make_bitwise [Offsetmap]

Maps from intervals to simple values.

Make_bitwise [Lmap_bitwise]
Make_list [Parameter_sig.Builder]
Make_map [Parameter_sig.Builder]

Parameter is a map where multibindings are **not** allowed.

Make_multiple_map [Parameter_sig.Builder]

Parameter is a map where multibindings are allowed.

Make_ordered [Hook]
Make_set [Parameter_sig.Builder]
Make_setter [Project_skeleton]
Make_table [Emitter]

Table indexing: key -> emitter (or equivalent data) -> value.

Make_tbl [Type]

Build an heterogeneous table associating keys to info.

Make_with_collections [Datatype]

Generic comparable datatype builder: functions equal, compare and hash must not be Datatype.undefined.

Map [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]
O
O [Lattice_type.Lattice_Set]
Obj_tbl [Type]

Heterogeneous table for the keys, but polymorphic for the values.

Offset [Cil_datatype]

Same remark as for Lval.

OffsetStructEq [Cil_datatype]
Offsetmap

Maps from intervals to values.

Offsetmap_bitwise_sig

Signature for Offsetmap_bitwise module, that implement efficient maps from intervals to values.

Offsetmap_lattice_with_isotropy

Type of the arguments of functor Offsetmap.Make

Offsetmap_sig

Signature for Offsetmap module, that implement efficient maps from intervals to arbitrary values.

Oneret
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]
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 full pretty-printer from a pretty-printing class.

Project

Projects management.

Project_manager

No function is exported.

Project_name [Gui_parameters]

Option -gui-project.

Project_skeleton

This module should not be used outside of the Project library.

Properties [Db]

Dealing with logical properties.

Property

ACSL comparable property.

Property_navigator

Extension of the GUI in order to navigate in ACSL properties.

Property_status

Status of properties.

Proxy [State_builder]

State proxy.

Q
Q [Transitioning]

Function Q.to_float was introduced in Zarith 1.5

Qstack

Mutable stack in which it is possible to add data at the end (like a queue) and to handle non top elements.

Quadruple [Datatype]
Quadruple_with_collections [Datatype]
Queue [State_builder]
Queue [Datatype]
Quiet [Kernel]

Behavior of option "-quiet"

R
Rangemap

Association tables over ordered types.

ReadAnnot [Kernel]

Behavior of option "-read-annot"

Record_From_Callbacks [Db.From]
Record_Value_After_Callbacks [Db.Value]
Record_Value_Callbacks [Db.Value]
Record_Value_Superposition_Callbacks [Db.Value]
Recursive [Structural_descr]

Use this module for handling a (possibly recursive) structural descriptor d.

Ref [State_builder]
Ref [Datatype]
Register [State_builder]

Register(Datatype)(State)(Info) registers a new state.

Register [Plugin]

Functors for registering a new plug-in.

Register [Log]

Each plugin has its own channel to output messages.

Rel [Abstract_interp]

"Relative" integers.

RemoveExn [Kernel]

Behavior of option "-remove-exn"

Reverse_binding [Journal]
Rgmap

Associative maps for _ranges_ to _values_ with overlapping.

Rich_text

Text with Tags

Rmtmps
RteGen [Db]

Runtime Error Annotation Generation plugin.

S
SafeArrays [Kernel]

Behavior of option "-safe-arrays".

SaveState [Kernel]

Behavior of option "-save"

Security [Db]

Security analysis.

Serializable_undefined [Datatype]

Same as Datatype.Undefined, but the type is supposed to be marshallable by the standard OCaml way (in particular, no hash-consing or projects inside the type).

Service_graph [Service_graph.S]
Service_graph

Compute services from a callgraph.

Session [Plugin.S_no_log]

Handle the specific `session' directory of the plug-in.

Session_dir [Kernel]

Directory in which session files are searched.

Set [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 Key.

Share [Plugin.S_no_log]

Handle the specific `share' directory of the plug-in.

SharedCounter [State_builder]

Creates a counter that is shared among all projects, but which is marshalling-compliant.

Sid [Cil]
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 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 [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.

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 f from String have been deprecated in favor of f_ascii, which operate only on the ASCII charset, while the deprecated f knew about iso-8859-1.

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

Ty_tbl [Type]

Heterogeneous tables indexed by type value.

Typ [Cil_datatype]

Types, with comparison over struct done by key and unrolling of typedefs.

TypByName [Cil_datatype]

Types, with comparison over struct done by name and no unrolling.

TypNoUnroll [Cil_datatype]

Types, with comparison over struct done by key and no unrolling

Type

Type value.

Type [Bottom]
TypeCheck [Kernel]

Behavior of option "-typecheck"

Type_namespace [Logic_typing]
Typed_parameter

Parameter settable through a command line option.

Typeinfo [Cil_datatype]
Types [Globals]

Types, or type-related information.

U
Undefined [Datatype]

Each values in these modules are undefined.

Undefined_sequence
Undo [Project]
Undo [Gui_parameters]

Option -undo.

Unicode

Handling unicode string.

Unicode [Kernel]

Behavior of option "-unicode".

Unit [Datatype]
Unmarshal

Provides a function input_val, similar in functionality to the standard library function Marshal.from_channel.

Unmarshal_z
UnrollUnnatural [Interpreted_automata]
Unroll_loops

Syntactic loop unrolling.

UnrollingForce [Kernel]

Behavior of option "-ulevel-force"

UnrollingLevel [Kernel]

Behavior of option "-ulevel"

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.

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]

Behavior of option "-warn-decimal-float"

Warning_manager

Handle Frama-C warnings in the GUI.

Wbox

Box Layouts.

Weak [Datatype]
Weak_hashtbl [State_builder]

Build a weak hashtbl over a datatype Data from a reference implementation W.

Wfile
Wide_string [Cil_datatype]
Widen_Hints [Ival]
Widget

Simple Widgets

WithOutput [Parameter_sig.Builder]
With_Cardinality [Map_lattice.Make_MapSet_Lattice]
With_Cardinality [Map_lattice.Make_Map_Lattice]
With_collections [Datatype]

Add sets, maps and hashtables modules to an existing datatype, provided the equal, compare and hash functions are not Datatype.undefined.

Wpalette
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

Z
Zero [Parameter_sig.Builder]
Zero_ref [State_builder]

Build a reference on an integer, initialized with 0.

Zone [Locations]

Association between bases and ranges of bits.