Module Cil_datatype

module Cil_datatype: sig .. end

Datatypes of some useful CIL types.


module UtilsFilepath: Filepath
module type S_with_pretty = sig .. end

Auxiliary module for datatypes that can be pretty-printed.

module type S_with_collections_pretty = sig .. end

Localisations

module Position: sig .. end

Single position in a file.

module Location: sig .. end

Cil locations.

module Localisation: Datatype.S  with type t = localisation
module Syntactic_scope: Datatype.S_with_collections  with type t = syntactic_scope

Cabs types

module Cabs_file: S_with_pretty  with type t = Cabs.file

C types

Sorted by alphabetic order.

module Block: S_with_pretty  with type t = block
module Compinfo: S_with_collections_pretty  with type t = compinfo
module Enuminfo: S_with_collections_pretty  with type t = enuminfo
module Enumitem: S_with_collections_pretty  with type t = enumitem
module Wide_string: S_with_collections  with type t = int64 list
module Constant: S_with_collections_pretty  with type t = constant
module Exp: sig .. end

Note that the equality is based on eid.

module ExpStructEq: S_with_collections  with type t = exp
module Fieldinfo: S_with_collections_pretty  with type t = fieldinfo
module File: S  with type t = file
module Global: sig .. end
module Initinfo: S_with_pretty  with type t = initinfo
module Instr: sig .. end
module Kinstr: sig .. end
module Label: S_with_collections_pretty  with type t = label
module Lval: S_with_collections_pretty  with type t = lval

Note that the equality is based on eid (for sub-expressions).

module LvalStructEq: S_with_collections  with type t = lval
module Offset: S_with_collections_pretty  with type t = offset

Same remark as for Lval.

module OffsetStructEq: S_with_collections  with type t = offset
module Stmt_Id: Hptmap.Id_Datatype  with type t = stmt
module Stmt: sig .. end
module Attribute: S_with_collections_pretty  with type t = attribute
module Attributes: S_with_collections  with type t = attributes
module Typ: sig .. end

Types, with comparison over struct done by key and unrolling of typedefs.

module TypByName: S_with_collections_pretty  with type t = typ

Types, with comparison over struct done by name and no unrolling.

module TypNoUnroll: S_with_collections_pretty  with type t = typ

Types, with comparison over struct done by key and no unrolling

module Typeinfo: S_with_collections  with type t = typeinfo
module Varinfo_Id: Hptmap.Id_Datatype  with type t = varinfo
module Varinfo: sig .. end
module Kf: sig .. end

ACSL types

Sorted by alphabetic order.

module Builtin_logic_info: S_with_collections_pretty  with type t = builtin_logic_info
module Code_annotation: sig .. end
module Funbehavior: S  with type t = funbehavior
module Funspec: S_with_pretty  with type t = funspec
module Fundec: S_with_collections_pretty  with type t = fundec
module Global_annotation: sig .. end
module Identified_term: S_with_collections_pretty  with type t = identified_term
module Logic_ctor_info: S_with_collections_pretty  with type t = logic_ctor_info
module Logic_info: S_with_collections_pretty  with type t = logic_info
module Logic_info_structural: S_with_collections_pretty  with type t = logic_info

Logic_info with structural comparison: name of the symbol, type of arguments Note that polymorphism is ignored, in the sense that two symbols with the same name and profile except for the name of their type variables will compare unequal.

module Logic_constant: S_with_collections_pretty  with type t = logic_constant
module Logic_label: S_with_collections_pretty  with type t = logic_label
module Logic_type: S_with_collections_pretty  with type t = logic_type

Logic_type.

module Logic_type_ByName: S_with_collections_pretty  with type t = logic_type
module Logic_type_NoUnroll: S_with_collections_pretty  with type t = logic_type
module Logic_type_info: S_with_collections_pretty  with type t = logic_type_info
module Logic_var: S_with_collections_pretty  with type t = logic_var
module Model_info: S_with_collections_pretty  with type t = model_info
module Term: S_with_collections_pretty  with type t = term
module Term_lhost: S_with_collections_pretty  with type t = term_lhost
module Term_offset: S_with_collections_pretty  with type t = term_offset
module Term_lval: S_with_collections_pretty  with type t = term_lval
module Logic_real: S_with_collections_pretty  with type t = logic_real
module Predicate: S_with_pretty  with type t = predicate
module Toplevel_predicate: S_with_pretty  with type t = toplevel_predicate
module Identified_predicate: S_with_collections_pretty  with type t = identified_predicate

Logic_ptree

Sorted by alphabetic order.

module Lexpr: S  with type t = Logic_ptree.lexpr

Beware: no pretty-printer is available.