Frama-C API - Frama_c_kernel
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 Async : sig ... end
Module dedicated to asynchronous actions.
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 Boot : sig ... end
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 Current_loc : 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 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 to perform dominators and postdominators analyses. This module was completely redesigned and provides many new functions.
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_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 Field : sig ... end
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 Finite : sig ... end
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 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 Inline_stmt_contracts : sig ... end
transforms requires and ensures of statement contracts into assert. This transformation is done after cleanup
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_type : sig ... end
Lattice signatures.
module Lexerhack : sig ... end
module Linear : sig ... end
module Linear_filter : sig ... end
module Linear_filter_test : 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 Machine : sig ... end
This module handle the machine configuration. Previous Frama-C versions handled this in Cil
.
module Macos_dirs : sig ... end
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 Nat : sig ... end
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 Option : sig ... end
module Ordered_stmt : sig ... end
module Origin : sig ... end
This module is used to track the origin of very imprecise values (namely "garbled mix", created on imprecise or unsupported operations on addresses) propagated by an Eva analysis.
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 Parray : 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 Result : sig ... end
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 System_config : sig ... end
Information about the environment
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 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 Unfold_loops : sig ... end
Syntactic loop unfolding. Uses code transformation hook mechanism (after-cleanup phase) of File
and exports nothing.
module Unicode : sig ... end
Handling unicode string.
module Unix_dirs : sig ... end
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 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 Win_dirs : sig ... end
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