Index of modules

Behavior of option "-absolute-valid-range"

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

Functors for generic lattices implementations.

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

Behavior of option "-aggressive-merging"

Alarms Database.

Generation of default allocates \nothing clauses.

Behavior of option "-allow-duplication".

Alpha conversion.

Nothing exported.

Annotations in the AST.

A collection is a standard string parameter

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

Behavior of option "-asm-contracts"

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

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

AST manipulation utilities.

List with constant-time concat operation.

Abstraction of the base of an addressable memory zone, together with the validity of the zone.

Behavior of option "-hexadecimal-big-integers"

Very low-level abstract functorial caches.

Some bit manipulations.

Bitvectors.

Boolean parameters.

Build a reference on a boolean.

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

Bounds a semi-lattice.

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

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

Untyped AST.

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

Helper functions for Cabs

Variable or function prototype name

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

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

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

Categories for this collection.

sets of category keywords

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

Behavior of option "-check"

CIL main API.

Smart constructors for some CIL data types

Datatypes of some useful CIL types.

Internal printer for Cabs2cil.

Internal Cil printer.

Functors for building computations which use kernel datatypes.

The Abstract Syntax of CIL.

Reading and storing configuration files from the filesystem.

The C Lexer.

Experimental module

Command line parsing.

Behavior of option "-ocode".

Useful high-level system operations.

Signatures for comparison operators ==, !=, <, >, <=, >=.

Default implementation for the Compositional_bool argument of the functor Hptmap.Make.

Actions to perform whenever a statement is handled.

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

Information about version of Frama-C.

Directory in which config files are searched.

Configuration module for the GUI: all magic visual constants should use this mechanism (window width, ratios, ...).

Consolidation of a property status according to the (consolidated) status of the hypotheses of the property.

See the consolidated status of a property in a graph, which all its dependencies and their consolidated status.

Global variables with "const" qualifier are constant.

Constant propagation plugin.

Behavior of option "-constfold"

Behavior of option "-continue-annot-error"

Behavior of option "-copy"

Creates a projectified counter.

Behavior of option "-cpp-command"

Behavior of option "-cpp-extra-args"

Behavior of option "-cpp-gnu-like"

Printers for the Cabs AST

forward reference to current location (see Cil.CurrentLoc)

A reference to the current location.

Behavior of option "-custom-annot-char".

Deprecated: use Dataflows instead.

Implementation of data flow analyses over user-supplied domains.

Implementation of data flow analyses over user-supplied domains.

A datatype provides useful values for types.

Database in which static plugins are registered.

prints debug messages having the corresponding key.

Nothing exported.

Type descriptor for safe unmarshalling.

Describe items of Source and Properties.

The extensible GUI.

Option -<short-name>-<specific-dir>.

Behavior of option "-collapse-call-cast".

Computation of dominators.

Value accesses through dynamic typing.

Emitter.

Behavior of option "-journal-enable"

Behavior of option "-enums"

The module stores the current file,line, and working directory in a hidden internal state, modified by the three following functions.

OCaml types used to represent wide characters and strings

Manages information related to possible exceptions thrown by each function in the AST.

Note that the equality is based on eid.

Useful operations.

Given a module that match the module type described above, F.build_cil_file initializes a new project containing the slices

Wrapper for Dynlink compatible with all OCaml versions.

Extension of OCaml's Hashtbl module.

Association tables over ordered types.

Sets over ordered types.

Build a reference on a boolean, initialized with false.

Lighter version than Consolidation

Bullets in left-margins

Frama-c preprocessing and Cil AST initialization.

Globals associated to filename.

Nothing exported.

This file performs various consistency checks over a cil file.

Functions manipulating filepaths.

Analyzed files

The tree containing the list of modules and functions together with dynamic columns

Filter helps to build a new cilfile from an old one by removing some of its elements.

Behavior of option "-float-hex"

Behavior of option "-float-normal"

Behavior of option "-float-relative"

Build a reference on a float.

Floating-point operations.

Behavior of option "-force-rl-arg-eval".

Behavior of option "-frama-c-stdlib"

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

Setting global, platform-wide settings.

Functional dependencies between function inputs and function outputs.

Signals that we are in MS VC mode

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

Operations on cil function.

Functions.

Floating-point intervals, used to construct arithmetic lattices.

Behavior of option "-debug"

Behavior of option "-verbose"

Operations on globals.

Group of command line options.

DEPRECATED.

Generic Gtk helpers.

Very early initialisation step required by any GUI.

GUI as a plug-in.

Special pretty-printers for the GUI.

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

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

Weak hashtbl dedicated to hashconsing.

Nothing exported.

Source code navigation history.

Hook builder.

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

Signature for the Hptmap module

Set of kernel functions.

Sets over ordered types.

Some generic icon management tools.

Impact analysis.

Behavior of option "-implicit-function-declaration"

Indexer implements ordered collection of items with random access.

Generation of possible assigns from the C prototype of a function.

Behavior of option "-initialized-padding-locals"

State_builder.of read inputs.

Integer parameters.

Big integers with an additional top element.

Sets of intervals with a lattice structure.

Sets of intervals with a lattice structure.

Build a reference on an integer.

Extension of Big_int compatible with Zarith.

Interpretation of logic terms.

Arithmetic lattices.

Kernel for journalization.

Journalization of functions.

Json Library

Behavior of option "-keep-switch"

Behavior of option "-keep-unused-specified-function".

Provided services for kernel developers.

Operations to get info from a kernel function.

As for Kernel_function_set, by default keys can only be defined functions.

As for Kernel_function_set, by default keys can only be defined functions.

Datatype for the keys of the hashtbl.

Datatype for the keys of the map.

Message and logging facility for abstract lattices.

Lattice signatures.

The Frama-C launcher.

Local logic environment

Behavior of option "-lib-entry".

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

Build a reference on a list.

Maps from bases to memory maps.

Functors making map indexed by zone.

Signature for maps from bases to memory maps.

Behavior of option "-load-module"

Behavior of option "-load"

Cil locations.

Sets of source locations

Association between bases and offsets in bits.

Association between bases and offsets in byte.

Memory locations.

Logging Services for Frama-C Kernel and Plugins.

Evaluation of logic terms and predicates

logic function/predicates that are effectively used in current project.

Smart contructors for logic annotations.

Global Logic Environment

Global Tables

All the interesting functions of this module are exported through Db.Interp.

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

Pretty-printing of a parsed logic tree.

logic constants.

Logic_type.

Logic typing and logic environment.

Utilities for ACSL constructs.

Operations on (natural) loops.

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

A functor to build custom Gtk lists.

Behavior of option "-machdep".

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

Frama-C main interface.

Behavior of option "-main".

Functor providing topological iterators over a graph.

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

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

Maps from intervals to values.

Make a new empty hook from unit.

Functor building an implementation of the set structure given a totally ordered type.

Functor building an implementation of the map structure given a totally ordered type.

Create a datatype for a monomorphic instance of the polymorphic type.

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

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

Generic datatype builder.

Datatype constructor.

See e.g.

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

Uncollapsed product.

Hashtable indexed by kernel functions and dealing with project.

Maps from intervals to simple values.

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

Parameter is a map where multibindings are allowed.

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

Build an heterogeneous table associating keys to info.

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

Map from a set of keys to values (a Lattice_With_Diff), equipped with the natural lattice interpretation.

Acces to slicing results.

Handle the menubar and the toolbar.

Merge a number of CIL files

Stored messages.

Behavior of option "-journal-name"

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

Interface for the occurrence plugin.

Same remark as for Lval.

Maps from intervals to values.

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

Type of the arguments of functor Offsetmap.Make

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

Make sure that there is only one Return statement in the whole body.

State_builder.of operational inputs.

Build a reference on an option.

An ordered_stmt is an int representing a stmt in a particular function.

Behavior of option "-orig-name"

The datastructures of this module can be used to track the origin of a major imprecision in the values of an abstract domain.

State_builder.of outputs.

Module to use for accessing parameters of plug-ins.

Functors for implementing new command line options.

Category for parameter collections.

Configuration of command line options.

Signatures for command line options.

Handling groups of parameters

Program Dependence Graph.

Provided plug-general services for plug-ins.

Generic implementation of polymorphic type value.

Functor for polymorphic types with only 1 type variable.

Generic implementation of polymorphic type value with two type variables.

Functor for polymorphic types with 2 type variables.

Generic implementation of polymorphic type value with three type variables.

Functor for polymorphic types with 3 type variables.

Generic implementation of polymorphic type value with four type variables.

Functor for polymorphic types with 4 type variables.

Single position in a file.

Syntaxic postdominators plugin.

Declarations common to the various postdominators-computing modules

Postdominators using value analysis results.

Behavior of option "-pp-annot"

Utilities to pretty print source with located elements in a Gtk TextBuffer.

Pretty-printer utilities.

Behavior of option "-print"

Behavior of option "-keep-comments"

Behavior of option "-print-config"

Behavior of option "-print-lib-path"

Behavior of option "-print-plugin-path"

Behavior of option "-print-share-path"

Behavior of option "-print-version"

AST's pretty-printer.

Type of AST's extensible printers.

Build a full pretty-printer from a pretty-printing class.

Projects management.

Slicing project management.

No function is exported.

Option -gui-project.

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

Dealing with logical properties.

ACSL comparable property.

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

Status of properties.

State proxy.

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

Behavior of option "-quiet"

Association tables over ordered types.

Behavior of option "-read-annot"

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

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

Functors for registering a new plug-in.

Each plugin has its own channel to output messages.

"Relative" integers.

Behavior of option "-remove-exn"

Dump Properties-Status consolidation tree.

Requests for slicing jobs.

Associative maps for _ranges_ to _values_ with overlaping.

removes unused labels for which is_removable is true.

Runtime Error Annotation Generation plugin.

Behavior of option "-safe-arrays".

Behavior of option "-save"

Interface for the Scope plugin.

Security analysis.

Slicing selections.

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

Compute services from a callgraph.

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

Directory in which session files are searched.

Undocumented.

This functor exports the shape of the maps indexed by keys Key.

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

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

Behavior of option "-warn-signed-downcast"

Behavior of option "-warn-signed-overflow"

Behavior of option "-simplify-cfg"

Behavior of option "-simplify-trivial-loops".

Function slice.

Interface for the slicing tool.

The source viewer multi-tabs widget window.

The Frama-C source viewer.

Interface for the unused code detection.

Nothing is exported: just register some special hooks for Frama-C.

This module can be used to instantiate the StmtStartData components of the functors below.

This module can be used to instantiate the StmtStartData components of the functors below.

A state is a project-compliant mutable value.

State builders.

State Dependency Graph.

A state selection is a set of states with operations for easy handling of state dependencies.

Topological ordering over states.

Operations over selections which depend on State_dependency_graph.graph.

Statuses of preconditions specialized at a given call-point.

For each block id, the data at the start.

For each statement id, the data at the start.

For each block id, the data at the start.

For each statement id, the data at the start.

Statements graph.

String parameters.

List of string parameters.

Set of string parameters.

Heterogeneous tables indexed by string.

Internal representations of OCaml type as first class values.

Behavior of option "-add-symbolic-path"

Table containing the results of the value analysis, ie.

High Level Interface to Command.

Option -gui-theme.

Behavior of option "-time"

Reduction of a location (expressed as an Ival.t and a size) by a base validity.

Traces.

Annotate files interpreting lightweight annotations.

Build a reference on a boolean, initialized with true.

Heterogeneous tables indexed by type value.

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

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

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

Type value.

Behavior of option "-typecheck"

Parameter settable through a command line option.

Types, or type-related information.

Each values in these modules are undefined.

Option -undo.

Handling unicode string.

Behavior of option "-unicode".

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

Extends Unmarshal to deal with the data types of the Nums library.

Syntactic loop unrolling.

Behavior of option "-ulevel-force"

Behavior of option "-ulevel"

Behavior of option "-warn-unsigned-downcast"

Behavior of option "-warn-unsigned-overflow"

Behavior of option "-unspecified-access"

Usable emitters are the ones which can really emit something.

Behavior of option "-unicode"

Functions used by another function.

UTF-8 string for logic symbols.

The Value analysis itself.

Globals variables.

Extensible Arrays

Frama-C visitors dealing with projects.

wto as Datatype

Behavior of option "-warn-decimal-float"

Handle Frama-C warnings in the GUI.

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

File Choosers

Simple Widgets

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

Panels

Table Views

Rich Text Renderer

Hierarchical Strongly Connected Components: performs Bourdoncle computation of a weak topological order on a graph represented by contiguous integers.

Weak topological ordering of statements.

Wtoolkit - Utilities

Build a reference on an integer, initialized with 0.

Association between bases and ranges of bits.