Functors for generic lattices implementations.

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

Lattice signatures using the Bottom type: these lattices do not include a bottom element, and return `Bottom instead when needed.

Implementation of floating-point values of different precision, using the standard ocaml floating-point numbers in double precision.

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.

Signature for the floating-point interval semantics.

Interface of floating-point numbers of different precisions.

Floating-point intervals, used to construct arithmetic lattices.

Big integers with an additional top element.

Sets of intervals with a lattice structure.

Sets of intervals with a lattice structure.

Integer intervals with congruence.

Small sets of integers.

Integer values abstractions: an abstraction represents a set of integers.

Arithmetic lattices.

Types, monads and utilitary functions for lattices in which the bottom and/or the top are managed separately from other values.

Message and logging facility for abstract lattices.

Lattice signatures.

Maps from bases to memory maps.

Functors making map indexed by zone.

Signature for maps from bases to memory maps.

Memory locations.

Maps equipped with a lattice structure.

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.

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

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

Some bit manipulations.

Implementation of data flow analyses over user-supplied domains.

Implementation of data flow analyses over user-supplied domains.

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.

Computation of dominators.

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

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

Operations on (natural) loops.

Compute services from a callgraph.

Statements graph.

Specialization of WTO for the CIL statement graph.

This module is meant to build C or ACSL expressions in a unified way.

Alarms Database.

Annotations in the AST.

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

The Abstract Syntax of CIL.

Operations on globals.

Operations to get info from a kernel function.

ACSL comparable property.

Status of properties.

Statuses of preconditions specialized at a given call-point.

Internal printer for Cabs2cil.

Internal Cil printer.

Printers for the Cabs AST

Describe items of Source and Properties.

Pretty-printing of a parsed logic tree.

AST's pretty-printer.

Type of AST's extensible printers.

Build a dynamic printer that bind all pretty-printers to the object obtained by (P())

Utilities to pretty print source with located Ast elements

ACSL extensions registration module

Compute diff information from an existing project.

AST manipulation utilities.

CIL main API.

Smart constructors for some CIL data types

Datatypes of some useful CIL types.

Functors for building computations which use kernel datatypes.

Frama-c preprocessing and Cil AST initialization.

This file performs various consistency checks over a cil file.

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

Smart constructors for logic annotations.

Global Logic Environment

Logic typing and logic environment.

Utilities for ACSL constructs.

Command line parsing.

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

Parameter settable through a command line option.

Untyped AST.

Helper functions for Cabs

logic constants.

Database in which static plugins are registered.

Value accesses through dynamic typing.

Emitter.

Journalization of functions.

Provided services for kernel developers.

Logging Services for Frama-C Kernel and Plugins.

Plugin registration and general services.

Frama-C visitors dealing with projects.

Operations on visitor behaviors.

A datatype provides useful values for types.

Type descriptor for safe unmarshalling.

Internal representations of OCaml type as first class values.

Type value.

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

Projects management.

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

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.

Useful operations.

Extension of OCaml's Hashtbl module.

Extension of Big_int compatible with Zarith.

This file contains functions available in recent OCaml releases but unavailable in the oldest OCaml version officially supported by Frama-C.

List with constant-time concat operation.

Very low-level abstract functorial caches.

Bitvectors.

Reading and storing configuration files from the filesystem.

Useful high-level system operations.

Helper for Printing Dot-graphs.

OCaml types used to represent wide characters and strings

Functions manipulating filepaths.

Floating-point operations.

Hook builder.

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

Signature for the Hptmap module

Sets over ordered types.

Indexer implements ordered collection of items with random access.

Json Library

Markdown Document Structured representation of Markdown content.

Pretty-printer utilities.

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

Association tables over ordered types.

Associative maps for _ranges_ to _values_ with overlapping.

Text with Tags

Sanitizer

High Level Interface to Command.

Handling unicode string.

UTF-8 string for logic symbols.

Extensible Arrays

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.

The C Lexer.

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

Lexer for logic annotations

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

Main entry point of Frama-C.

Information about version of Frama-C.

Setting global, platform-wide settings.

Very early initialization step required by any GUI.

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

Stored messages for persistence between sessions.

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

Generation of default allocates \nothing clauses.

Alpha conversion.

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

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

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

Signals that we are in MS VC mode

Checks that memory accesses are well-typed in the sense of the \ghost qualifier.

Checks that normal cfg is not altered by ghost statements.

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

Merge a number of CIL files

A visitor that substitutes globals, defined with the attribute 'const', with respective initializers.

Annotate files interpreting lightweight annotations.

Syntactic loop unrolling.

Nothing exported.

The extensible GUI.

Creation of windows for displaying graphs.

Nothing exported.

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

DEPRECATED.

Generic Gtk helpers.

GUI as a plug-in.

Special pretty-printers for the GUI.

Nothing exported.

Source code navigation history.

The Frama-C launcher.

Handle the menubar and the toolbar.

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

No function is exported.

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

The source viewer multi-tabs widget window.

The Frama-C source viewer.

Handle Frama-C warnings in the GUI.

Box Layouts.

Simple Widgets

Panels

Table Views

Rich Text Renderer

Wtoolkit - Utilities

once f returns a function that will only be applied once per execution of the program and returns the same value afterwards.