Abstract_interp | Functors for generic lattices implementations. |
Base | Abstraction of the base of an addressable memory zone, together with the validity of the zone. |
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_bounds | Types, monads and utilitary functions for lattices in which the bottom and/or the top are managed separately from other values. |
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_lattice_with_isotropy | Type of the arguments of functor |
Offsetmap_sig | Signature for |
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 |
Dominators | Computation of dominators. |
Exn_flow | Manages information related to possible exceptions thrown by each function in the AST. |
Interpreted_automata | |
Logic_interp | All the interesting functions of this module are exported through
|
Loop | Operations on (natural) loops. |
Ordered_stmt | |
Service_graph | Compute services from a callgraph. |
Stmts_graph | Statements graph. |
Undefined_sequence | |
Wto_statement | Specialization of WTO for the CIL statement graph. |
Cil_builder | This module is meant to build C or ACSL expressions in a unified way. |
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_diff | Compute diff information from an existing project. |
Ast_info | AST manipulation utilities. |
Cil | CIL main API. |
Cil_builtins | |
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 |
|
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 | |
Contract_special_float | |
Filter | |
Inline |
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 | Plugin registration and general services. |
Cabsvisit | |
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 |
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 |
Integer | Extension of |
Transitioning | This file contains functions available in recent OCaml releases but unavailable 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 |
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 | Lexer for logic annotations |
Logic_parser | |
Logic_preprocess | adds another pre-processing step in order to expand macros in annotations. |
Parse_env |
Boot | Main entry point of Frama-C. |
Dump_config | |
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 |
Messages | Stored messages for persistence between sessions. |
Special_hooks | Nothing is exported: just register some special hooks for Frama-C. |
Allocates | Generation of default |
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_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 | |
Rmtmps | |
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 | Creation of windows for displaying graphs. |
File_manager | Nothing exported. |
Filetree | The tree containing the list of modules and functions together with dynamic columns |
GSourceView | |
Gtk_compat | |
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 | |
Widget | Simple Widgets |
Wpalette | |
Wpane | Panels |
Wtable | Table Views |
Wtext | Rich Text Renderer |
Wutil | Wtoolkit - Utilities |
Wutil_once |
|