Frama-C:
Plug-ins:
Libraries:

Frama-C API - Fclib

module Ansi_escape : sig ... end

This modules provides utilities to use semantic tags to output color and style information on capable terminals.

module Array : sig ... end

Extension of OCaml's Stdlib.Array module.

module Async : sig ... end

Module dedicated to asynchronous actions.

module Bag : sig ... end

List with constant-time concat operation.

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

Bitvectors.

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

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

Helper for Printing Dot-graphs.

module Escape : sig ... end
module Extlib : sig ... end

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

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

This module handle locations in a source file. Fileloc.t is a Frama-C datatype, and comes with usual compare, equal, hash and pretty functions.

module Filepath : sig ... end

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

module Filepos : sig ... end

This module handle positions in a source file. Filepos.t is a Frama-C datatype, and comes with usual compare, equal, hash and pretty functions.

module Filesystem : sig ... end

The set of functions in Filesystem are provided both as a convenient way to use Filepath.t directly (without conversion) and to be safer variants than the standard library's or Unix library's.

module Finite : sig ... end

Encoding of finite set in OCaml type system.

module Floating_point : sig ... end
module Fun : sig ... end

Extension of OCaml's Stdlib.Fun module.

module Hash : sig ... end

This module provides hash functions.

module Hashtbl : sig ... end

Extension of OCaml's Stdlib.Hashtbl module.

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

Extension of OCaml's Stdlib.Int module.

module Integer : sig ... end

This module is deprecated, use Z instead. Extension of Zarith module Z.

module Json : sig ... end

Json Library

module Linear : sig ... end

Definition of a linear space over a field.

module List : sig ... end

Extension of OCaml's Stdlib.List module. @see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

module Log : sig ... end

Logging Services for Frama-C Kernel and Plugins.

module Lti_system : sig ... end

This module aims to provide overapproximations of the behaviors of linear time-invariant systems, for both the transition and the permanent phases.

module Map : sig ... end

Extension of OCaml's Stdlib.Maps module.

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

Extension of OCaml's Stdlib.Option module. Be wary that the parameters order of the bind function are reversed compared to the standard library and that get takes an optional exn argument. @see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

module Parray : sig ... end
module Pretty : sig ... end

This module provides pretty printing utilities. Same as Pretty_utils but without dependencies to Fclib.List or Fclib.Array.

module Pretty_utils : sig ... end

Pretty-printer utilities.

module Project : sig ... end

Projects management.

module Project_skeleton : sig ... end

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

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 Rich_text : sig ... end
module Sanitizer : sig ... end
module Set : sig ... end

Extension of OCaml's Stdlib.Set module.

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

Extension of OCaml's Stdlib.String module.

module Structural_descr : sig ... end

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

module Task : sig ... end

High Level Interface to Command.

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

Pretty printers of unicode symbols. Each function in this module prints a single unicode symbol, or an ASCII-based replacement if -no-unicode option is set.

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. Use the Unicode module to print these symbols.

module Vector : sig ... end

Extensible Arrays

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

Extension of Z from Zarith. Fc_internal_z only includes to Zarith.Z module, it is mandatory if we want to call this module Z without shadowing Zarith's module. This solution is a bit ugly and could be replace by root_module in kernel dune file, but this does not work for now...