package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Abstract_interp : sig ... end

Functors for generic lattices implementations.

module Acsl_extension : sig ... end

ACSL extensions registration module

module Alarms : sig ... end

Alarms Database.

module Allocates : sig ... end

Generation of default allocates \nothing clauses.

module Alpha : sig ... end

Alpha conversion.

module Annotations : sig ... end

Annotations in the AST. The AST should be computed before calling functions of this module.

module Asm_contracts : sig ... end

Code transformation for inferring contracts from information given in GNU's extended assembly syntax. Registered as a transformation occurring after annotations table are filled.

module Ast : sig ... end

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

module Ast_diff : sig ... end

Compute diff information from an existing project.

module Ast_info : sig ... end

AST manipulation utilities.

module Bag : sig ... end

List with constant-time concat operation.

module Base : sig ... end

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

module Binary_cache : sig ... end

Very low-level abstract functorial caches. Do not use them unless you understand what happens in this module, and do not forget that those caches are not aware of projects.

module Bit_utils : sig ... end

Some bit manipulations.

module Bitvector : sig ... end

Bitvectors.

module Cabs : sig ... end

Untyped AST.

module Cabs2cil : sig ... end
module Cabs_debug : sig ... end
module Cabshelper : sig ... end

Helper functions for Cabs

module Cabsvisit : sig ... end
module Cfg : sig ... end

Code to compute the control-flow graph of a function or file. This will fill in the preds and succs fields of Cil_types.stmt

module Cil : sig ... end

CIL main API.

module Cil_builder : sig ... end

This module is meant to build C or ACSL expressions in a unified way. Compared to "classic" Cil functions it also avoid the necessity to provide a location everywhere.

module Cil_builtins : sig ... end
module Cil_const : sig ... end
module Cil_datatype : sig ... end

Datatypes of some useful CIL types.

module Cil_descriptive_printer : sig ... end

Internal printer for Cabs2cil.

module Cil_printer : sig ... end

Internal Cil printer.

module Cil_state_builder : sig ... end

Functors for building computations which use kernel datatypes.

module Cil_types : sig ... end

The Abstract Syntax of CIL.

module Cil_types_debug : sig ... end
module Cilconfig : sig ... end

Reading and storing configuration files from the filesystem. Currently only used in Frama-C's GUI.

module Clexer : sig ... end

The C Lexer.

module Clone : sig ... end

Experimental module

module Cmdline : sig ... end

Command line parsing.

module Command : sig ... end

Useful high-level system operations.

module Config_data : sig ... end
module Contract_special_float : sig ... end
module Cparser : sig ... end
module Cprint : sig ... end
module Cvalue : sig ... end

Representation of Value's abstract memory.

module Dataflow2 : sig ... end

Implementation of data flow analyses over user-supplied domains.

module Dataflows : sig ... end

Implementation of data flow analyses over user-supplied domains.

module Datatype : sig ... end

A datatype provides useful values for types. It is a high-level API on top of module Type.

module Db : sig ... end

Database in which static plugins are registered.

module Descr : sig ... end

Type descriptor for safe unmarshalling.

module Description : sig ... end

Describe items of Source and Properties.

module Destructors : sig ... end

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.

module Dominators : sig ... end
module Dotgraph : sig ... end

Helper for Printing Dot-graphs.

module Dump_config : sig ... end
module Dynamic : sig ... end

Value accesses through dynamic typing.

module Dyncall : sig ... end
module Emitter : sig ... end

Emitter. An emitter is the Frama-C entity which is able to emit annotations and property status. Thus you have to create (at least) one of your own if you want to do such tasks.

module Errorloc : sig ... end

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

module Escape : sig ... end
module Eva_lattice_type : sig ... end

Lattice signatures using the Bottom type: these lattices do not include a bottom element, and return `Bottom instead when needed. Except that, they are identical to the module signatures in Lattice_type.

module Exn_flow : sig ... end

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

module Extlib : sig ... end

Useful operations. This module does not depend of any of frama-c module.

module FCHashtbl : sig ... end

Extension of OCaml's Hashtbl module.

module Fc_config : sig ... end

Information about version of Frama-C. The body of this module is generated from Makefile.

module Fc_float : sig ... end

Implementation of floating-point values of different precision, using the standard ocaml floating-point numbers in double precision. Long_Double and Real are inexact.

module File : sig ... end

Frama-c preprocessing and Cil AST initialization.

module Filecheck : sig ... end

This file performs various consistency checks over a cil file. Code may vary depending on current development of the kernel and/or identified bugs.

module Filepath : sig ... end

Functions manipulating filepaths. In these functions, references to the current working directory refer to the result given by function Sys.getcwd.

module Filter : sig ... end

Filter helps to build a new cilfile from an old one by removing some of * its elements. One can even build several functions from a source function * by specifying different names for each of them. *

module Float_interval : sig ... end
module Float_interval_sig : sig ... end

Signature for the floating-point interval semantics.

module Float_sig : sig ... end

Interface of floating-point numbers of different precisions.

module Floating_point : sig ... end

Floating-point operations.

module Frontc : sig ... end
module Function_Froms : sig ... end

Datastructures and common operations for the results of the From plugin.

module Fval : sig ... end

Floating-point intervals, used to construct arithmetic lattices. The interfaces of this module may change between Frama-C versions. Contact us if you need stable APIs.

module Ghost_accesses : sig ... end
module Ghost_cfg : sig ... end
module Globals : sig ... end

Operations on globals.

module Hook : sig ... end

Hook builder. A hook is a bunch of functions which can be extended and applied at any program point.

module Hptmap : sig ... end

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

module Hptmap_sig : sig ... end

Signature for the Hptmap module

module Hptset : sig ... end

Sets over ordered types.

module Indexer : sig ... end

Indexer implements ordered collection of items with random access. It is suitable for building fast access operations in GUI tree and list widgets.

module Infer_assigns : sig ... end

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

module Inline : sig ... end
module Inout_type : sig ... end
module Int_Base : sig ... end

Big integers with an additional top element.

module Int_Intervals : sig ... end

Sets of intervals with a lattice structure. Consecutive intervals are automatically fused.

module Int_Intervals_sig : sig ... end

Sets of intervals with a lattice structure. Consecutive intervals are automatically fused.

module Int_interval : sig ... end

Integer intervals with congruence. An interval defined by min, max, rem, modu represents all integers between the bounds min and max and congruent to rem modulo modu. A value of None for min (resp. max) represents -infinity (resp. +infinity). modu is > 0, and 0 <= rem < modu.

module Int_set : sig ... end

Small sets of integers.

module Int_val : sig ... end

Integer values abstractions: an abstraction represents a set of integers. Provided with a lattice structure and over-approximations of arithmetic operations.

module Integer : sig ... end

Extension of Big_int compatible with Zarith.

module Interpreted_automata : sig ... end

An interpreted automaton is a convenient formalization of programs for abstract interpretation. It is a control flow graph where states are control point and edges are transitions. It keeps track of conditions on which a transition can be taken (guards) as well as actions which are computed when a transition is taken. It can then be interpreted w.r.t. the operational semantics to reproduce the behavior of the program or w.r.t. to the collection semantics to compute a set of reachable states.

module Ival : sig ... end

Arithmetic lattices. The interfaces of this module may change between Frama-C versions. Contact us if you need stable APIs.

module Json : sig ... end

Json Library

module Json_compilation_database : sig ... end
module Kernel : sig ... end

Provided services for kernel developers.

module Kernel_function : sig ... end

Operations to get info from a kernel function. This module does not give access to information about the set of all the registered kernel functions (like iterators over kernel functions). This kind of operations is stored in module Globals.Functions.

module Lattice_bounds : sig ... end

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

module Lattice_messages : sig ... end

Message and logging facility for abstract lattices.

module Lattice_type : sig ... end

Lattice signatures.

module Lexerhack : sig ... end
module Lmap : sig ... end

Maps from bases to memory maps. The memory maps are those of the Offsetmap module.

module Lmap_bitwise : sig ... end

Functors making map indexed by zone.

module Lmap_sig : sig ... end

Signature for maps from bases to memory maps. The memory maps are intended to be those of the Offsetmap module.

module Locations : sig ... end

Memory locations.

module Log : sig ... end

Logging Services for Frama-C Kernel and Plugins.

module Logic_builtin : sig ... end
module Logic_const : sig ... end

Smart constructors for logic annotations.

module Logic_deps : sig ... end
module Logic_env : sig ... end
module Logic_lexer : sig ... end

Lexer for logic annotations

module Logic_parse_string : sig ... end
module Logic_parser : sig ... end
module Logic_preprocess : sig ... end

adds another preprocessing step in order to expand macros in annotations.

module Logic_print : sig ... end

Pretty-printing of a parsed logic tree.

module Logic_ptree : sig ... end
module Logic_to_c : sig ... end
module Logic_typing : sig ... end

Logic typing and logic environment.

module Logic_utils : sig ... end

Utilities for ACSL constructs.

module Loop : sig ... end

Operations on (natural) loops.

module Machdep : sig ... end

Managing machine-dependent information.

module Map_lattice : sig ... end

Maps equipped with a lattice structure.

module Markdown : sig ... end
module Mergecil : sig ... end
module Messages : sig ... end

Stored messages for persistence between sessions.

module Offsetmap : sig ... end

Maps from intervals to values.

module Offsetmap_bitwise_sig : sig ... end

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

module Offsetmap_lattice_with_isotropy : sig ... end

Type of the arguments of functor Offsetmap.Make

module Offsetmap_sig : sig ... end

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

module Oneret : sig ... end
module Ordered_stmt : sig ... end
module Origin : sig ... end

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

module Parameter_builder : sig ... end

Functors for implementing new command line options.

module Parameter_category : sig ... end

Category for parameter collections. A category groups together a set of possible values of a given type for some parameters. It may be created once and used several times.

module Parameter_customize : sig ... end

Configuration of command line options.

module Parameter_sig : sig ... end

Signatures for command line options.

module Parameter_state : sig ... end
module Parse_env : sig ... end
module Plugin : sig ... end

Plugin registration and general services.

module Populate_spec : sig ... end

This module is used to generate missing specifications. Options Kernel.GeneratedDefaultSpec, Kernel.GeneratedSpecMode and Kernel.GeneratedSpecCustom can be used to choose precisely which clause to generate in which case.

module Precise_locs : sig ... end

This module provides transient datastructures that may be more precise than an Ival.t, Locations.Location_Bits.t and Locations.location respectively, typically for l-values such as t[i][j], p->t[i], etc. Those structures do not have a lattice structure, and cannot be stored as an abstract domain. However, they can be use to model more precisely read or write accesses to semi-imprecise l-values.

module Pretty_utils : sig ... end

Pretty-printer utilities.

module Printer : sig ... end

AST's pretty-printer.

module Printer_api : sig ... end

Type of AST's extensible printers.

module Printer_builder : sig ... end

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

module Printer_tag : sig ... end

Utilities to pretty print source with located Ast elements

module Project : sig ... end

Projects management.

module Project_skeleton : sig ... end

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

module Property : sig ... end

ACSL comparable property.

module Property_status : sig ... end

Status of properties.

module Qstack : sig ... end

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

module Rangemap : sig ... end

Association tables over ordered types.

module Rgmap : sig ... end

Associative maps for _ranges_ to _values_ with overlapping.

module Rich_text : sig ... end

Text with Tags

module Rmtmps : sig ... end
module Sanitizer : sig ... end
module Service_graph : sig ... end

Compute services from a callgraph.

module Special_hooks : sig ... end

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

module State : sig ... end

A state is a project-compliant mutable value.

module State_builder : sig ... end

State builders. Provide ways to implement signature State_builder.S. Depending on the builder, also provide some additional useful information.

module State_dependency_graph : sig ... end

State Dependency Graph.

module State_selection : sig ... end

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

module State_topological : sig ... end

Topological ordering over states.

module Statuses_by_call : sig ... end

Statuses of preconditions specialized at a given call-point.

module Stmts_graph : sig ... end

Statements graph.

module Structural_descr : sig ... end

Internal representations of OCaml type as first class values. These values are called structural descriptors.

module Substitute_const_globals : sig ... end
module Task : sig ... end

High Level Interface to Command.

module Tr_offset : sig ... end

Reduction of a location (expressed as an Ival.t and a size) by a base validity. Only the locations in the trimmed result are valid. All offsets are expressed in bits.

module Transitioning : sig ... end

This file contains functions available in recent OCaml releases but unavailable in the oldest OCaml version officially supported by Frama-C. Be sure to update it when support for a given version is dropped.

module Translate_lightweight : sig ... end

Annotate files interpreting lightweight annotations.

module Type : sig ... end

Type value. A type value is a value representing a static ML monomorphic type. This API is quite low level. Prefer to use module Datatype instead whenever possible.

module Typed_parameter : sig ... end

Parameter settable through a command line option. This is a low level API, internally used by the kernel. As a plug-in developer, you certainly prefer to use the API of Plugin instead.

module Undefined_sequence : sig ... end
module Unicode : sig ... end

Handling unicode string.

module Unmarshal : sig ... end

Provides a function input_val, similar in functionality to the standard library function Marshal.from_channel. The main difference with Marshal.from_channel is that input_val is able to apply transformation functions on the values on the fly as they are read from the input channel.

module Unmarshal_z : sig ... end
module Unroll_loops : sig ... end

Syntactic loop unrolling. Uses code transformation hook mechanism (after-cleanup phase) of File and exports nothing.

module Utf8_logic : sig ... end

UTF-8 string for logic symbols.

module Vector : sig ... end

Extensible Arrays

module Visitor : sig ... end

Frama-C visitors dealing with projects.

module Visitor_behavior : sig ... end

Operations on visitor behaviors.

module Widen_type : sig ... end

Widening hints for the Value Analysis datastructures.

module Wto : sig ... end

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. This is a very convenient representation to describe an evaluation order to reach a fixpoint.

module Wto_statement : sig ... end

Specialization of WTO for the CIL statement graph. See the Wto module for more details