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.
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.
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.
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.
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.
Logic_interp
All the interesting functions of this module are exported through Db.Interp.
Loop
Operations on (natural) loops.
Ordered_stmt
An ordered_stmt is an int representing a stmt in a particular function.
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 full pretty-printer from a pretty-printing class.

Section Ast_queries (in src/kernel_services/ast_queries)


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.
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
Experimental module
Filter
Filter helps to build a new cilfile from an old one by removing some of its elements.

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
Provided plug-general services for plug-ins.

Section Visitors (in src/kernel_services/visitors)


Cabsvisit
Variable or function prototype name
Visitor
Frama-C visitors dealing with projects.

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.
FCBuffer
Extensible buffers.
FCHashtbl
Extension of OCaml's Hashtbl module.
FCMap
Association tables over ordered types.
FCSet
Sets over ordered types.
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.
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
Leftistheap
Leftist heaps.
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.
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)


Config
Information about version of Frama-C.
Frama_c_init
Setting global, platform-wide settings.
Gui_init
Very early initialisation 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
Infer_annotations
Generation of possible assigns from the C prototype of a function.
Logic_builtin
Mergecil
Merge a number of CIL files
Oneret
Make sure that there is only one Return statement in the whole body.
Rmtmps
removes unused labels for which is_removable is true.
Translate_lightweight
Annotate files interpreting lightweight annotations.
Unroll_loops
Syntactic loop unrolling.

Directory plugins

Section Gui (in plugins/gui)


Analyses_manager
Nothing exported.
Debug_manager
Nothing exported.
Design
The extensible GUI.
File_manager
Nothing exported.
Filetree
The tree containing the list of modules and functions together with dynamic columns
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
File Choosers
Widget
Simple Widgets
Wpalette
A side-bar palette of tools.
Wpane
Panels
Wtable
Table Views
Wtext
Rich Text Renderer
Wutil
Wtoolkit - Utilities