Module Frama_c_kernel.Cil_datatype

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. For those that do not have this signature, module Printer must be used.

module type S_with_collections_pretty = sig ... end

Localisations

module Position : sig ... end

Single position in a file.

module Location : sig ... end

Cil locations.

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 = Cil_types.block
module Wide_string : Datatype.S_with_collections with type t = int64 list
module Constant : sig ... end

Same as 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. For structural equality, use ExpStructEq

structural equality, with strict constant comparison as in ConstantStrict

module File : Datatype.S with type t = Cil_types.file
module Global : sig ... end
module Instr : sig ... end
module Kinstr : sig ... end

Note that the equality is based on eid (for sub-expressions). For structural equality, use LvalStructEq

structural equality, with strict constant comparison as in ConstantStrict

Same remark as for Lval. For structural equality, use OffsetStructEq.

structural equality, with strict constant comparison as in ConstantStrict

module Stmt : sig ... end
module Typ : sig ... end

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

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

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

Types, with comparison over struct done by key and ignoring attributes.

module Varinfo : sig ... end
module Kf : sig ... end

ACSL types

Sorted by alphabetic order.

module Code_annotation : sig ... end
module Global_annotation : sig ... end

Logic_info with structural comparison:

Logic_type. See the various Typ* modules for the distinction between those modules

Logic_ptree

Sorted by alphabetic order.

module Lexpr : Datatype.S with type t = Logic_ptree.lexpr

Beware: no pretty-printer is available.