Abstract_interp |
Functors for generic lattices implementations.
|
Base |
Abstraction of the base of an addressable memory zone, together with
the validity of the zone.
|
Bottom |
Types, monads and utilitary functions for lattices in which the bottom is
managed separately from other values.
|
Eva_lattice_type |
Lattice signatures using the Bottom type:
these lattices do not include a bottom element, and return `Bottom instead
when needed.
|
Fc_float |
Implementation of floating-point values of different precision,
using the standard ocaml floating-point numbers in double precision.
|
Float_interval |
Builds a semantics of floating-point intervals for different precisions,
from a module providing the floating-point numbers used for the bounds
of the intervals.
|
Float_interval_sig |
Signature for the floating-point interval semantics.
|
Float_sig |
Interface of floating-point numbers of different precisions.
|
Fval |
Floating-point intervals, used to construct arithmetic lattices.
|
Int_Base |
Big integers with an additional top element.
|
Int_Intervals |
Sets of intervals with a lattice structure.
|
Int_Intervals_sig |
Sets of intervals with a lattice structure.
|
Int_interval |
Integer intervals with congruence.
|
Int_set |
Small sets of integers.
|
Int_val |
Integer values abstractions: an abstraction represents a set of integers.
|
Ival |
Arithmetic lattices.
|
Lattice_messages |
Message and logging facility for abstract lattices.
|
Lattice_type |
Lattice signatures.
|
Lmap |
Maps from bases to memory maps.
|
Lmap_bitwise |
Functors making map indexed by zone.
|
Lmap_sig |
Signature for maps from bases to memory maps.
|
Locations |
Memory locations.
|
Map_lattice |
Maps equipped with a lattice structure.
|
Offsetmap |
Maps from intervals to values.
|
Offsetmap_bitwise_sig |
Signature for
Offsetmap_bitwise module, that implement efficient maps
from intervals to values.
|
Offsetmap_lattice_with_isotropy |
Type of the arguments of functor
Offsetmap.Make
|
Offsetmap_sig |
Signature for
Offsetmap module, that implement efficient maps from
intervals to arbitrary values.
|
Origin |
The datastructures of this module can be used to track the origin
of a major imprecision in the values of an abstract domain.
|
Tr_offset |
Reduction of a location (expressed as an Ival.t and a size)
by a base validity.
|
Bit_utils |
Some bit manipulations.
|
Dataflow2 |
Implementation of data flow analyses over user-supplied domains.
|
Dataflows |
Implementation of data flow analyses over user-supplied domains.
|
Destructors |
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.
|
Dominators |
Computation of dominators.
|
Exn_flow |
Manages information related to possible exceptions thrown by each
function in the AST.
|
Interpreted_automata |
An interpreted automaton is a convenient formalization of programs for
abstract interpretation.
|
Logic_interp |
All the interesting functions of this module are exported through
Db.Interp .
|
Loop |
Operations on (natural) loops.
|
Ordered_stmt |
An
ordered_stmt is an int representing a stmt in a particular
function.
|
Service_graph |
Compute services from a callgraph.
|
Stmts_graph |
Statements graph.
|
Undefined_sequence | |
Wto_statement |
Specialization of WTO for the CIL statement graph.
|
Alarms |
Alarms Database.
|
Annotations |
Annotations in the AST.
|
Ast |
Access to the CIL AST which must be used from Frama-C.
|
Cil_types |
The Abstract Syntax of CIL.
|
Globals |
Operations on globals.
|
Kernel_function |
Operations to get info from a kernel function.
|
Property |
ACSL comparable property.
|
Property_status |
Status of properties.
|
Statuses_by_call |
Statuses of preconditions specialized at a given call-point.
|
Cabs_debug | |
Cil_descriptive_printer |
Internal printer for Cabs2cil.
|
Cil_printer |
Internal Cil printer.
|
Cil_types_debug | |
Cprint |
Printers for the Cabs AST
|
Description |
Describe items of Source and Properties.
|
Logic_print |
Pretty-printing of a parsed logic tree.
|
Printer |
AST's pretty-printer.
|
Printer_api |
Type of AST's extensible printers.
|
Printer_builder |
Build a dynamic printer that bind all pretty-printers to the
object obtained by (P())
|
Printer_tag |
Utilities to pretty print source with located Ast elements
|
Acsl_extension |
ACSL extensions registration module
|
Ast_info |
AST manipulation utilities.
|
Cil |
CIL main API.
|
Cil_const |
Smart constructors for some CIL data types
|
Cil_datatype |
Datatypes of some useful CIL types.
|
Cil_state_builder |
Functors for building computations which use kernel datatypes.
|
File |
Frama-c preprocessing and Cil AST initialization.
|
Filecheck |
This file performs various consistency checks over a cil file.
|
Json_compilation_database | get_flags f returns the preprocessing flags associated to file f
in the JSON compilation database (when enabled), or the empty string
otherwise.
|
Logic_const |
Smart constructors for logic annotations.
|
Logic_env |
Global Logic Environment
|
Logic_typing |
Logic typing and logic environment.
|
Logic_utils |
Utilities for ACSL constructs.
|
Clone |
Experimental module
|
Filter | Filter helps to build a new cilfile from an old one by removing some of
its elements.
|
Inline | inline_term ~inline term inlines in term the application of predicates
and logic functions for which inline is true.
|
Cmdline |
Command line parsing.
|
Parameter_builder |
Functors for implementing new command line options.
|
Parameter_category |
Category for parameter collections.
|
Parameter_customize |
Configuration of command line options.
|
Parameter_sig |
Signatures for command line options.
|
Parameter_state |
Handling groups of parameters
|
Typed_parameter |
Parameter settable through a command line option.
|
Cabs |
Untyped AST.
|
Cabshelper |
Helper functions for Cabs
|
Logic_ptree |
logic constants.
|
Db |
Database in which static plugins are registered.
|
Dynamic |
Value accesses through dynamic typing.
|
Emitter |
Emitter.
|
Journal |
Journalization of functions.
|
Kernel |
Provided services for kernel developers.
|
Log |
Logging Services for Frama-C Kernel and Plugins.
|
Plugin |
Special signature for Kernel services, whose messages are handled in
an ad'hoc manner.
|
Cabsvisit |
Variable or function prototype
name
|
Visitor |
Frama-C visitors dealing with projects.
|
Visitor_behavior |
Operations on visitor behaviors.
|
Datatype |
A datatype provides useful values for types.
|
Descr |
Type descriptor for safe unmarshalling.
|
Structural_descr |
Internal representations of OCaml type as first class values.
|
Type |
Type value.
|
Unmarshal |
Provides a function
input_val , similar in
functionality to the standard library function Marshal.from_channel .
|
Unmarshal_z |
Project |
Projects management.
|
Project_skeleton |
This module should not be used outside of the Project library.
|
State |
A state is a project-compliant mutable value.
|
State_builder |
State builders.
|
State_dependency_graph |
State Dependency Graph.
|
State_selection |
A state selection is a set of states with operations for easy handling of
state dependencies.
|
State_topological |
Topological ordering over states.
|
Extlib |
Useful operations.
|
FCHashtbl |
Extension of OCaml's
Hashtbl module.
|
Integer |
Extension of
Big_int compatible with Zarith .
|
Transitioning |
This file contains functions that uses features that are deprecated in
current OCaml version, but whose replacing feature is not available in
the oldest OCaml version officially supported by Frama-C.
|
Bag |
List with constant-time concat operation.
|
Binary_cache |
Very low-level abstract functorial caches.
|
Bitvector |
Bitvectors.
|
Cilconfig |
Reading and storing configuration files from the filesystem.
|
Command |
Useful high-level system operations.
|
Dotgraph |
Helper for Printing Dot-graphs.
|
Escape |
OCaml types used to represent wide characters and strings
|
Filepath |
Functions manipulating filepaths.
|
Floating_point |
Floating-point operations.
|
Hook |
Hook builder.
|
Hptmap |
Efficient maps from hash-consed trees to values, implemented as
Patricia trees.
|
Hptmap_sig |
Signature for the
Hptmap module
|
Hptset |
Sets over ordered types.
|
Indexer |
Indexer implements ordered collection of items with
random access.
|
Json |
Json Library
|
Markdown |
Markdown Document
Structured representation of Markdown content.
|
Pretty_utils |
Pretty-printer utilities.
|
Qstack |
Mutable stack in which it is possible to add data at the end (like a queue)
and to handle non top elements.
|
Rangemap |
Association tables over ordered types.
|
Rgmap |
Associative maps for _ranges_ to _values_ with overlapping.
|
Rich_text |
Text with Tags
|
Sanitizer |
Sanitizer
|
Task |
High Level Interface to Command.
|
Unicode |
Handling unicode string.
|
Utf8_logic |
UTF-8 string for logic symbols.
|
Vector |
Extensible Arrays
|
Wto |
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.
|
Clexer |
The C Lexer.
|
Cparser | |
Errorloc |
The module stores the current file,line, and working directory in a
hidden internal state, modified by the three following
functions.
|
Lexerhack | |
Logic_lexer | |
Logic_parser | |
Logic_preprocess |
adds another pre-processing step in order to expand macros in
annotations.
|
Fc_config |
Information about version of Frama-C.
|
Frama_c_init |
Setting global, platform-wide settings.
|
Gui_init |
Very early initialization step required by any GUI.
|
Machdeps |
Some predefined
Cil_types.mach which specifies machine-dependent
data about C programs.
|
Messages |
Stored messages for persistence between sessions.
|
Special_hooks |
Nothing is exported: just register some special hooks for Frama-C.
|
Allocates |
Generation of default
allocates \nothing clauses.
|
Alpha |
Alpha conversion.
|
Asm_contracts |
Code transformation for inferring contracts from information given
in GNU's extended assembly syntax.
|
Cabs2cil |
Registers a new hook that will be applied each time a side-effect free
expression whose result is unused is dropped.
|
Cfg |
Code to compute the control-flow graph of a function or file.
|
Frontc |
Signals that we are in MS VC mode
|
Ghost_accesses |
Checks that memory accesses are well-typed in the sense of the
\ghost
qualifier.
|
Ghost_cfg |
Checks that normal cfg is not altered by ghost statements.
|
Infer_annotations |
Generation of possible assigns from the C prototype of a function.
|
Logic_builtin | |
Mergecil |
Merge a number of CIL files
|
Oneret |
If there are local variables with destructors belonging to the main block
of
f , encapsulate_local_vars f will move ret , the return
statement of f outside of this main block (changing f.sbody to
a two-statement block composed of the old block and ret ) to
avoid having gotos to ret bypassing the initialization of these variables.
|
Rmtmps |
removes unused labels for which
is_removable is true.
|
Substitute_const_globals |
A visitor that substitutes globals, defined with the attribute 'const', with
respective initializers.
|
Translate_lightweight |
Annotate files interpreting lightweight annotations.
|
Unroll_loops |
Syntactic loop unrolling.
|
Analyses_manager |
Nothing exported.
|
Design |
The extensible GUI.
|
Dgraph_helper |
Create a new window displaying a graph.
|
File_manager |
Nothing exported.
|
Filetree |
The tree containing the list of modules and functions together with dynamic columns
|
GSourceView | |
Gtk_compat |
makes the font smaller.
|
Gtk_form |
DEPRECATED.
|
Gtk_helper |
Generic Gtk helpers.
|
Gui_parameters |
GUI as a plug-in.
|
Gui_printers |
Special pretty-printers for the GUI.
|
Help_manager |
Nothing exported.
|
History |
Source code navigation history.
|
Launcher |
The Frama-C launcher.
|
Menu_manager |
Handle the menubar and the toolbar.
|
Pretty_source |
Utilities to pretty print source with located elements in a Gtk
TextBuffer.
|
Project_manager |
No function is exported.
|
Property_navigator |
Extension of the GUI in order to navigate in ACSL properties.
|
Source_manager |
The source viewer multi-tabs widget window.
|
Source_viewer |
The Frama-C source viewer.
|
Warning_manager |
Handle Frama-C warnings in the GUI.
|
Wbox |
Box Layouts.
|
Wfile |
File Choosers
|
Widget |
Simple Widgets
|
Wpalette |
A side-bar palette of tools.
|
Wpane |
Panels
|
Wtable |
Table Views
|
Wtext |
Rich Text Renderer
|
Wutil |
Wtoolkit - Utilities
|
Wutil_once | once f returns a function that will only be applied once per
execution of the program and returns the same value afterwards.
|