package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Analyses : sig ... end

General module for E-ACSL analyses

module Analyses_datatype : sig ... end

Datatypes for analyses types

module Analyses_types : sig ... end

Types used by E-ACSL analyses

module Assert : sig ... end

Module with the context to hold the data contributing to an assertion and general functions to create assertion statements.

module Assigns : sig ... end
module Bound_variables : sig ... end
module Builtins : sig ... end

E-ACSL built-in database.

module Contract : sig ... end

Translate a given ACSL contract (function or statement) into the corresponding C statement for runtime assertion checking.

module Contract_types : sig ... end
module E_acsl_visitor : sig ... end
module Env : sig ... end
module Error : sig ... end

Handling errors.

module Exit_points : sig ... end

E-ACSL tracks a local variable by injecting:

module Functions : sig ... end
module Global_observer : sig ... end

Observation of global variables.

module Gmp : sig ... end

Calls to the GMP's API.

module Gmp_types : sig ... end

GMP Values.

module Injector : sig ... end

The E-ACSL main instrumentation step.

module Interval : sig ... end

Interval inference for terms.

module Labels : sig ... end

Pre-analysis for Labeled terms and predicates.

module Libc : sig ... end

Code generation for libc functions

module Literal_observer : sig ... end

Observation of literal strings in C expressions.

module Literal_strings : sig ... end

Associate literal strings to fresh varinfo.

module Local_config : sig ... end
module Logic_aggr : sig ... end

Utilities function for aggregate types.

module Logic_array : sig ... end
module Logic_functions : sig ... end

Generate C implementations of user-defined logic functions. A logic function can have multiple C implementations depending on the types computed for its arguments. Eg: Consider the following definition: integer g(integer x) = x with the following calls: g(5) and g(10*INT_MAX) They will respectively generate the C prototypes int g_1(int) and long g_2(long)

module Logic_normalizer : sig ... end

This module is dedicated to some preprocessing on the predicates:

module Loops : sig ... end

Loop specific actions.

module Lscope : sig ... end
module Main : sig ... end

Register the plugin in the Frama-C kernel. Nothing is exported.

module Memory_observer : sig ... end

Extend the environment with statements which allocate/deallocate memory blocks.

module Memory_tracking : sig ... end

Compute a sound over-approximation of what left-values must be tracked by the memory model library

module Memory_translate : sig ... end
module Misc : sig ... end

Utilities for E-ACSL.

module Options : sig ... end
module Prepare_ast : sig ... end

Prepare AST for E-ACSL generation.

module Quantif : sig ... end

Convert quantifiers.

module Rte : sig ... end

Accessing the RTE plug-in easily.

module Rtl : sig ... end

This module links the E-ACSL's RTL to the user source code.

module Smart_exp : sig ... end
module Smart_stmt : sig ... end
module Temporal : sig ... end

Transformations to detect temporal memory errors (e.g., dereference of stale pointers).

module Translate_annots : sig ... end

Functions that translate a given ACSL annotation into the corresponding C statements (if any) for runtime assertion checking. These C statements are part of the resulting environment.

module Translate_ats : sig ... end

Generate C implementations of E-ACSL \at() terms and predicates.

module Translate_predicates : sig ... end

Generate C implementations of E-ACSL predicates.

module Translate_rtes : sig ... end

Generate and translate RTE annotations.

module Translate_terms : sig ... end

Generate C implementations of E-ACSL terms.

module Translate_utils : sig ... end

Utility functions for generating C implementations.

module Translation_error : sig ... end
module Typed_number : sig ... end

Manipulate the type of numbers.

module Typing : sig ... end

Type system which computes the smallest C type that may contain all the possible values of a given integer term or predicate. Also compute the required casts. It is based on interval inference of module Interval.

module Varname : sig ... end
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct