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-30.0-beta-Zinc.tar.gz

sha256=93a291a8764644df2f3618d7ea18258b5fbe0912ec98dfdfd180967afdf24474

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_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.

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

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