Frama-C API - `Frama_c_kernel_base`

module Abstract_interp : sig ... end

Functors for generic lattices implementations.

module Acsl_extension : sig ... end

ACSL extensions registration module

module Addresses : sig ... end

Represent a set of addresses by associating bases with offsets.

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_attributes : sig ... end

This file contains attribute related types/functions/values.

module Ast_diff : sig ... end

Compute diff information from an existing project.

module Ast_info : sig ... end

AST manipulation utilities.

module Ast_types : sig ... end

This file contains types related types/functions/values.

module Base : sig ... end

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

module Bit_utils : sig ... end

Some bit manipulations.

module Boot : sig ... end

module Builder : 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 avoids 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 Classify : sig ... end

module Clexer : sig ... end

The C Lexer.

module Clone : sig ... end

Experimental module

module Cmdline : sig ... end

Command line parsing.

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 Demote_string_literal : sig ... end

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 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 Environment : sig ... end

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 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 Extends : sig ... end

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 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 Format_parser : sig ... end

module Format_pprint : sig ... end

module Format_string : sig ... end

module Format_typer : sig ... end

module Format_types : sig ... end

See C11, 7.21.6

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 Generic : sig ... end

module Ghost_accesses : sig ... end

module Ghost_cfg : sig ... end

module Globals : sig ... end

Operations on globals.

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

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 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_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 Kernel_log : sig ... end

This modules creates Kernel Logs manually instead of using the one created via the Plugin modules. It is required for Cmdline which cannot depend on Plugin. It also includes all Kernel debug and warning keys. Unless you cannot depend on Frama-C's kernel, always prefer using Kernel instead of Kernel_log.

module Lattice_bounds : sig ... end

Types, monads and utility 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 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 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_subst : sig ... end

Substitution of formals in terms and predicates. These operations are intended for replacing formal parameters by actual ones in terms or predicates occurring in a C function pre-conditions at call site.

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 Memory_zone : sig ... end

Association between bases and ranges of bits.

module Mergecil : sig ... end

module Messages : sig ... end

Stored messages for persistence between sessions.

module Mopsa_database : 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 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 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, Addresses.Bits.t and Locations.t 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 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 Property : sig ... end

ACSL comparable property.

module Property_status : sig ... end

Status of properties.

module Replacements : sig ... end

module Rmtmps : 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 Standard : sig ... end

module Statuses_by_call : sig ... end

Statuses of preconditions specialized at a given call-point.

module Stmts_graph : sig ... end

Statements graph.

module Substitute_const_globals : sig ... end

module System_config : sig ... end

Information about the environment

module Temp_files : sig ... end

This module provides a layer above the Filesystem module to handle automatic removal of temporary files when the program exits, except when exit is caused by a signal or keep is given and set to true. If keep is omitted, the files are kept only if the kernel option -keep-temp-files is set. If the file is kept, a message with the path of the preserved file or directory is emitted. When the temporary file or directory cannot be created, these functions abort.

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 : sig ... end

module Translate_lightweight : sig ... end

Annotate files interpreting lightweight annotations.

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 Unix_dirs : sig ... end

module Va_types : sig ... end

module Variadic : sig ... end

Nothing is exported.

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_statement : sig ... end

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

module Z_or_top : sig ... end

Z integers with an additional top element.

Frama-C API - Frama_c_kernel_base

Frama-C API - `Frama_c_kernel_base`