package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

dune-project

Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-31.0-Gallium.tar.gz

sha256=a94384f00d53791cbb4b4d83ab41607bc71962d42461f02d71116c4ff6dca567

doc/frama-c.kernel/Frama_c_kernel/index.html

Module `Frama_c_kernel`Source

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

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

This module exposes two functors that, given a monad T called the "interior monad" and a monad S called the "exterior monad", build a monad of type 'a T.t S.t. To be able to do so, one has to provide a swap function that, simply put, swap the exterior monad out of the interior one. In other word, this function allows fixing "badly ordered" monads compositions, in the sens that they are applied in the opposite order as the desired one.

module Compression : sig ... end

File compression.

Sourcemodule 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

This module provides a generic signature describing mathematical fields, i.e algebraic structure that behave like rationals, reals or complex numbers. The signature also provides several functions that are not directly part of fields definition, but are useful nonetheless, in particular when using fields to model floating point computations.

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 normalized filepaths. In these functions, references *he current working directory refer to the result given by function Sys.getcwd.

module Filesystem : sig ... end

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

Encoding of finite set in OCaml type system.

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

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

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

Definition of a linear space over a field. Used by Linear_filter to represent and compute linear filters invariants.

module Linear_filter : sig ... end

Compute filters invariants, i.e bounds for each of the filter's state dimensions when the iterations goes to infinity.

module Linear_filter_test : sig ... end

module List : sig ... end

Extend the list type to a full fleshed monad. This monad can be used to represent non-deterministic computations.

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

This module provides generic signatures for monads along with tools to build them based on minimal definitions. Those tools are provided for advanced users that would like to define their own monads. Any user that only wants to use the monads provided by the kernel can completly ignore them.

module Nat : sig ... end

Encoding of the Peano arithmetic in OCaml type system. A value of type n nat contains n at the value and the type level, allowing to express properties on objects sizes and accesses for example. It is used by the module Linear to represent vectors and matrices dimensions.

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

Extend the option type to a full fleshed monad. Be wary that the parameters order of the bind function are reversed compared to the standard library.

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

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

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

Implementation of the Field signature based on rational numbers.

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

The State monad represents computations relying on a global mutable state but implemented in a functionnal way.

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 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 if exit is caused by a signal and except if keep is given and set to true. If keep is omitted, the files are only kept if the debug key Kernel.dkey_pp_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_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_float : sig ... end

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