Frama-C Kernel

Chapter 1. Kernel Services

Section Abstract_interp (in src/kernel_services/abstract_interp)


Abstract_interp

Functors for generic lattices implementations.

Base

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

Bottom

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

Eva_lattice_type

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

Fc_float

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

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_sig

Interface of floating-point numbers of different precisions.

Fval

Floating-point intervals, used to construct arithmetic lattices.

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_interval

Integer intervals with congruence.

Int_set

Small sets of integers.

Int_val

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

Ival

Arithmetic lattices.

Lattice_messages

Message and logging facility for abstract lattices.

Lattice_type

Lattice signatures.

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.

Locations

Memory locations.

Map_lattice

Maps equipped with a lattice structure.

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.

Origin

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

Tr_offset

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

Section Analysis (in src/kernel_services/analysis)


Bit_utils

Some bit manipulations.

Dataflow2

Implementation of data flow analyses over user-supplied domains.

Dataflows

Implementation of data flow analyses over user-supplied domains.

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.

Dominators

Computation of dominators.

Exn_flow

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

Interpreted_automata
Logic_interp

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

Loop

Operations on (natural) loops.

Ordered_stmt
Service_graph

Compute services from a callgraph.

Stmts_graph

Statements graph.

Undefined_sequence
Wto_statement

Specialization of WTO for the CIL statement graph.

Section Ast_data (in src/kernel_services/ast_data)


Alarms

Alarms Database.

Annotations

Annotations in the AST.

Ast

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

Cil_types

The Abstract Syntax of CIL.

Globals

Operations on globals.

Kernel_function

Operations to get info from a kernel function.

Property

ACSL comparable property.

Property_status

Status of properties.

Statuses_by_call

Statuses of preconditions specialized at a given call-point.

Section Ast_printing (in src/kernel_services/ast_printing)


Cabs_debug
Cil_descriptive_printer

Internal printer for Cabs2cil.

Cil_printer

Internal Cil printer.

Cil_types_debug
Cprint

Printers for the Cabs AST

Description

Describe items of Source and Properties.

Logic_print

Pretty-printing of a parsed logic tree.

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

Section Ast_queries (in src/kernel_services/ast_queries)


Acsl_extension

ACSL extensions registration module

Ast_info

AST manipulation utilities.

Cil

CIL main API.

Cil_const

Smart constructors for some CIL data types

Cil_datatype

Datatypes of some useful CIL types.

Cil_state_builder

Functors for building computations which use kernel datatypes.

File

Frama-c preprocessing and Cil AST initialization.

Filecheck

This file performs various consistency checks over a cil file.

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.

Logic_const

Smart constructors for logic annotations.

Logic_env

Global Logic Environment

Logic_typing

Logic typing and logic environment.

Logic_utils

Utilities for ACSL constructs.

Section Ast_transformations (in src/kernel_services/ast_transformations)


Clone
Filter
Inline

Section Cmdline_parameters (in src/kernel_services/cmdline_parameters)


Cmdline

Command line parsing.

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

Typed_parameter

Parameter settable through a command line option.

Section Parsetree (in src/kernel_services/parsetree)


Cabs

Untyped AST.

Cabshelper

Helper functions for Cabs

Logic_ptree

logic constants.

Section Plugin_entry_points (in src/kernel_services/plugin_entry_points)


Db

Database in which static plugins are registered.

Dynamic

Value accesses through dynamic typing.

Emitter

Emitter.

Journal

Journalization of functions.

Kernel

Provided services for kernel developers.

Log

Logging Services for Frama-C Kernel and Plugins.

Plugin

Special signature for Kernel services, whose messages are handled in an ad'hoc manner.

Section Visitors (in src/kernel_services/visitors)


Cabsvisit
Visitor

Frama-C visitors dealing with projects.

Visitor_behavior

Operations on visitor behaviors.

Chapter 2. Libraries

Section Datatype (in src/libraries/datatype)


Datatype

A datatype provides useful values for types.

Descr

Type descriptor for safe unmarshalling.

Structural_descr

Internal representations of OCaml type as first class values.

Type

Type value.

Unmarshal

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

Unmarshal_z

Section Project (in src/libraries/project)


Project

Projects management.

Project_skeleton

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

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.

Section Stdlib (in src/libraries/stdlib)


Extlib

Useful operations.

FCHashtbl

Extension of OCaml's Hashtbl module.

Integer

Extension of Big_int compatible with Zarith.

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.

Section Utils (in src/libraries/utils)


Bag

List with constant-time concat operation.

Binary_cache

Very low-level abstract functorial caches.

Bitvector

Bitvectors.

Cilconfig

Reading and storing configuration files from the filesystem.

Command

Useful high-level system operations.

Dotgraph

Helper for Printing Dot-graphs.

Escape

OCaml types used to represent wide characters and strings

Filepath

Functions manipulating filepaths.

Floating_point

Floating-point operations.

Hook

Hook builder.

Hptmap

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

Hptmap_sig

Signature for the Hptmap module

Hptset

Sets over ordered types.

Indexer

Indexer implements ordered collection of items with random access.

Json

Json Library

Markdown

Markdown Document Structured representation of Markdown content.

Pretty_utils

Pretty-printer utilities.

Qstack

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

Rangemap

Association tables over ordered types.

Rgmap

Associative maps for _ranges_ to _values_ with overlapping.

Rich_text

Text with Tags

Sanitizer

Sanitizer

Task

High Level Interface to Command.

Unicode

Handling unicode string.

Utf8_logic

UTF-8 string for logic symbols.

Vector

Extensible Arrays

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.

Chapter 3. Kernel Internals

Section Parsing (in src/kernel_internals/parsing)


Clexer

The C Lexer.

Cparser
Errorloc

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

Lexerhack
Logic_lexer
Logic_parser
Logic_preprocess

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

Section Runtime (in src/kernel_internals/runtime)


Dump_config
Fc_config

Information about version of Frama-C.

Frama_c_init

Setting global, platform-wide settings.

Gui_init

Very early initialization step required by any GUI.

Machdeps

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

Messages

Stored messages for persistence between sessions.

Special_hooks

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

Section Typing (in src/kernel_internals/typing)


Allocates

Generation of default allocates \nothing clauses.

Alpha

Alpha conversion.

Asm_contracts

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

Cabs2cil

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

Cfg

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

Frontc

Signals that we are in MS VC mode

Ghost_accesses

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

Ghost_cfg

Checks that normal cfg is not altered by ghost statements.

Infer_annotations

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

Logic_builtin
Mergecil

Merge a number of CIL files

Oneret
Rmtmps
Substitute_const_globals

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

Translate_lightweight

Annotate files interpreting lightweight annotations.

Unroll_loops

Syntactic loop unrolling.

Directory plugins

Section Gui (in plugins/gui)


Analyses_manager

Nothing exported.

Design

The extensible GUI.

Dgraph_helper

Create a new window displaying a graph.

File_manager

Nothing exported.

Filetree

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

GSourceView
Gtk_compat
Gtk_form

DEPRECATED.

Gtk_helper

Generic Gtk helpers.

Gui_parameters

GUI as a plug-in.

Gui_printers

Special pretty-printers for the GUI.

Help_manager

Nothing exported.

History

Source code navigation history.

Launcher

The Frama-C launcher.

Menu_manager

Handle the menubar and the toolbar.

Pretty_source

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

Project_manager

No function is exported.

Property_navigator

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

Source_manager

The source viewer multi-tabs widget window.

Source_viewer

The Frama-C source viewer.

Warning_manager

Handle Frama-C warnings in the GUI.

Wbox

Box Layouts.

Wfile
Widget

Simple Widgets

Wpalette
Wpane

Panels

Wtable

Table Views

Wtext

Rich Text Renderer

Wutil

Wtoolkit - Utilities

Wutil_once

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