Frama-C Kernel


Chapter 1. Frama-C

Section Ai (in src/ai)


Abstract_interp
Functors for generic lattices implementations.
Base
Abstraction of the base of an addressable memory zone, together with the validity of the zone.
Int_Base
Big integers with an additional top element.
Ival
Arithmetic lattices.
Lattice_Interval_Set
Sets of disjoint intervals with a lattice structure.
Lattice_type
Lattice signatures.
Map_Lattice
Map from a set of keys to values (a Lattice_With_Diff), equipped with the natural lattice interpretation.
Origin
The datastructures of this module can be used to track the origin of a major imprecision in the values of an abstract domain.
Trace

Section Buckx (in src/buckx)


Buckx
Undocumented.

Section Gui (in src/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.
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.
Toolbox
GUI Toolbox.
Warning_manager
Handle Frama-C warnings in the GUI.

Section Kernel (in src/kernel)


Alarms
Alarms Database.
Ast
Access to the CIL AST which must be used from Frama-C.
Ast_info
AST manipulation utilities.
CilE
CIL Extension for Frama-C.
Cmdline
Command line parsing.
Command
Useful high-level system operations.
Config
Information about version of Frama-C.
Db
Database in which static plugins are registered.
Dominators
Computation of dominators.
Dynamic
Dynamic plug-ins: registration and use.
Emitter
Emitter.
File
Frama-c preprocessing and Cil AST initialization.
Globals
Operations on globals.
Gui_init
Very early initialisation step required by any GUI.
Journal
Journalization of functions.
Kernel
Provided services for kernel developers.
Kernel_function
Operations to get info from a kernel function.
Log
Logging Services for Frama-C Kernel and Plugins.
Loop
Operations on (natural) loops.
Messages
Stored messages.
Parameter_builder
Functors for implementing new command line options.
Parameter_customize
Configuration of command line options.
Parameter_sig
Signatures for command line options.
Parameter_state
Handling groups of parameters
Plugin
Provided plug-general services for plug-ins.
Special_hooks
Nothing is export: just register some special hooks for Frama-C.
Stmts_graph
Statements graph.
Task
High Level Interface to Command.
Typed_parameter
Parameter settable through a command line option.
Unicode
Handling unicode string.
Unroll_loops
Syntactic loop unrolling.
Visitor
Frama-C visitors dealing with projects.

Section Lib (in src/lib)


Bag
List with constant-time concat operation.
Binary_cache
Very low-level abstract functorial caches.
Bitvector
Bitvector naive implementation.
Dynlink_common_interface
Wrapper for Dynlink compatible with all OCaml versions.
Extlib
Useful operations.
FCHashtbl
Extension of OCaml's Hashtbl module.
FCMap
Association tables over ordered types.
FCSet
Sets over ordered types.
Filepath
Functions manipulating filepaths.
Floating_point
Floating-point operations.
Hook
Hook builder.
Hptset
Sets over ordered types.
Indexer
Indexer implements ordered collection of items with random access.
Integer
Extension of Big_int compatible with Zarith.
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.
Vector
Extensible Arrays

Section Logic (in src/logic)


Allocates
Generation of default allocates \nothing clauses.
Annotations
Annotations in the AST.
Description
Describe items of Source and Properties.
Infer_annotations
Generation of possible assigns from the C prototype of a function.
Logic_interp
Undocumented.
Property
ACSL comparable property.
Property_status
Status of properties.
Statuses_by_call
Statuses of preconditions specialized at a given call-point.
Translate_lightweight
Annotate files interpreting lightweight annotations.

Section Memory_state (in src/memory_state)


Cvalue
Representation of Value's abstract memory.
Function_Froms
Datastructures and common operations for the results of the From plugin.
Int_Interv
Intervals of integers.
Int_Interv_Map
Undocumented.
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.
Offsetmap
Maps from intervals to values.
Offsetmap_bitwise
Undocumented.
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.
Tr_offset
Reduction of a location (expressed as an Ival.t and a size) by a base validity.
Value_messages
Value_types
Declarations that are useful for plugins written on top of the results of Value.
Widen_type
Widening hints for the Value Analysis datastructures.

Section Misc (in src/misc)


Bit_utils
Some bit manipulations.
Filter
Filter helps to build a new cilfile from an old one by removing some of its elements.
Service_graph
Compute services from a callgraph.

Section Printer (in src/printer)


Cil_descriptive_printer
Internal printer for Cabs2cil.
Cil_printer
Internal Cil printer.
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 Project (in src/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 Type (in src/type)


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.

Chapter 2. C & ACSL

Section Ext (in cil/ext)


Availexpslv
Callgraph
Compute a static call graph.
Cfg
Code to compute the control-flow graph of a function or file.
Dataflow
A framework for implementing data flow analysis.
Dataflow2
A framework for implementing data flow analysis.
Dataflows
Deadcodeelim
Dead code elimination.
Expcompare
Liveness
Oneret
Make sure that there is only one Return statement in the whole body.
Ordered_stmt
An ordered_stmt is an int representing a stmt in a particular function.
Reachingdefs
Rmciltmps
Usedef
compute use/def information

Section Frontc (in cil/frontc)


Cabs
This file was originally part of Hugues Casee's frontc 2.0, and has been extensively changed since.
Cabs2cil
Registers a new hook that will be applied each time a side-effect free expression whose result is unused is dropped.
Cabs_debug
Cabsbranches
Force the link for branches
Cabscond
Interface to be used during Cabs2cil
Cabshelper
Helper functions for Cabs
Cabsvisit
Variable or function prototype name
Clexer
The C Lexer.
Cparser
Cprint
Printers for the Cabs AST
Errorloc
This function is used especially when the preprocessor has generated linemarkers in the output that let us know the current working directory at the time of preprocessing (option -fworking-directory for GNU CPP).
Frontc
Signals that we are in MS VC mode
Lexerhack

Section Logic (in cil/logic)


Logic_builtin
Logic_const
Smart contructors for logic annotations.
Logic_env
Global Logic Environment
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_typing
Logic typing and logic environment.
Logic_utils
Utilities for ACSL constructs.
Utf8_logic
UTF-8 string for logic symbols.

Section Ocamlutil (in cil/ocamlutil)


Alpha
Alpha conversion.
Cilconfig
Reading and storing configuration files from the filesystem.

Section Src (in cil/src)


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.
Cil_types
The Abstract Syntax of CIL.
Cilmsg
CIL's internal stack of errors.
Escape
OCaml types used to represent wide characters and strings
Mergecil
Merge a number of CIL files
Rmtmps
removes unused labels for which is_removable is true.

Directory frama-c

Section External (in frama-c/external)


Hptmap
Efficient maps from hash-consed trees to values, implemented as Patricia trees.
Sysutil
System utilities (filename management, etc).
Unmarshal
Provides a function input_val, similar in functionality to the standard library function Marshal.from_channel.
Unmarshal_nums
Extends Unmarshal to deal with the data types of the Nums library.