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
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
module Cabs_file:S_with_pretty
with type t = Cabs.file
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:sig
..end
module ConstantStrict:S_with_collections
with type t = constant
Same as Cil_datatype.Constant
, but comparison is strict, in the sense that it will take
into account textual representation if provided.
module Exp:sig
..end
Note that the equality is based on eid.
module ExpStructEq:S_with_collections
with type t = exp
module ExpStructEqStrict:S_with_collections
with type t = exp
structural equality, with strict constant comparison as in Cil_datatype.ConstantStrict
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 LvalStructEqStrict:S_with_collections
with type t = lval
structural equality, with strict constant comparison as in Cil_datatype.ConstantStrict
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 OffsetStructEqStrict:S_with_collections
with type t = offset
structural equality, with strict constant comparison as in Cil_datatype.ConstantStrict
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 TypNoAttrs:S_with_collections_pretty
with type t = typ
Types, with comparison over struct done by key and ignoring attributes.
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
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_pretty
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
module PredicateStructEq:S_with_collections_pretty
with type t = predicate
Sorted by alphabetic order.
module Lexpr:S
with type t = Logic_ptree.lexpr
Beware: no pretty-printer is available.