Frama-C API - `Cil_datatype`

Datatypes of some useful CIL types.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

module UtilsFilepath = Filepath

This module should not be exported, but we need the alias and OCaml requires us to export it.

module type S_with_collections = sig ... end

All datatypes in this module include a dummy.

module type S = sig ... end

All datatypes in this module include a dummy.

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.

module Syntactic_scope : S_with_collections with type t = Cil_types.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 = Cil_types.block

module Compinfo : S_with_collections_pretty with type t = Cil_types.compinfo

module Enuminfo : S_with_collections with type t = Cil_types.enuminfo

module Enumitem : S_with_collections with type t = Cil_types.enumitem

module Wide_string : S_with_collections with type t = int64 list

module Constant : S_with_collections_pretty with type t = Cil_types.constant

module ConstantStrict : S_with_collections with type t = Cil_types.constant

Same as Constant, but comparison is strict, in the sense that it will take into account textual representation if provided.

module Exp : S_with_collections_pretty with type t = Cil_types.exp

Note that the equality is based on eid. For structural equality, use ExpStructEq

module ExpStructEq : S_with_collections with type t = Cil_types.exp

module ExpStructEqStrict : S_with_collections with type t = Cil_types.exp

Structural equality, with strict constant comparison as in ConstantStrict

module ExpStructEqSized : S_with_collections with type t = Cil_types.exp

Structural equality, with structural comparison in case of sizeof (instead of id). Different expressions with the same size within sizeof are equal.

module ExpStructEqStrictSized : S_with_collections with type t = Cil_types.exp

Structural equality, with strict constant comparison as in ConstantStrict and with structural comparison in case of sizeof (instead of id). Different expressions with the same size within sizeof are equal.

module Fieldinfo : S_with_collections_pretty with type t = Cil_types.fieldinfo

module File : S with type t = Cil_types.file

module Global : sig ... end

module Initinfo : S_with_pretty with type t = Cil_types.initinfo

module Instr : sig ... end

module Kinstr : sig ... end

module Label : S_with_collections_pretty with type t = Cil_types.label

module Lval : S_with_collections_pretty with type t = Cil_types.lval

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

module LvalStructEq : S_with_collections with type t = Cil_types.lval

module LvalStructEqStrict : S_with_collections with type t = Cil_types.lval

structural equality, with strict constant comparison as in ConstantStrict

module Offset : S_with_collections_pretty with type t = Cil_types.offset

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

module OffsetStructEq : S_with_collections with type t = Cil_types.offset

module OffsetStructEqStrict : S_with_collections with type t = Cil_types.offset

structural equality, with strict constant comparison as in ConstantStrict

module Stmt_Id : Hptmap.Id_Datatype with type t = Cil_types.stmt

module Stmt : sig ... end

module Attribute : S_with_collections_pretty with type t = Cil_types.attribute

module Attributes : S_with_collections with type t = Cil_types.attributes

module Typ : S_with_collections_pretty with type t = Cil_types.typ

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

module TypByName : S_with_collections_pretty with type t = Cil_types.typ

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

module TypNoUnroll : S_with_collections_pretty with type t = Cil_types.typ

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

module TypNoAttrs : S_with_collections_pretty with type t = Cil_types.typ

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

module Typeinfo : S_with_collections with type t = Cil_types.typeinfo

module Varinfo_Id : Hptmap.Id_Datatype with type t = Cil_types.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 = Cil_types.builtin_logic_info

module Code_annotation : sig ... end

module Funbehavior : S_with_pretty with type t = Cil_types.funbehavior

module Funspec : S_with_pretty with type t = Cil_types.funspec

module Fundec : S_with_collections_pretty with type t = Cil_types.fundec

module Global_annotation : sig ... end

module Identified_term : S_with_collections_pretty with type t = Cil_types.identified_term

module Logic_ctor_info : S_with_collections_pretty with type t = Cil_types.logic_ctor_info

module Logic_info : S_with_collections_pretty with type t = Cil_types.logic_info

module Logic_info_structural : S_with_collections_pretty with type t = Cil_types.logic_info

Logic_info with structural comparison:

module Logic_constant : S_with_collections_pretty with type t = Cil_types.logic_constant

module Logic_label : S_with_collections_pretty with type t = Cil_types.logic_label

module Logic_type : S_with_collections_pretty with type t = Cil_types.logic_type

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

module Logic_type_ByName : S_with_collections_pretty with type t = Cil_types.logic_type

module Logic_type_NoUnroll : S_with_collections_pretty with type t = Cil_types.logic_type

module Logic_type_info : S_with_collections_pretty with type t = Cil_types.logic_type_info

module Logic_var : S_with_collections_pretty with type t = Cil_types.logic_var

module Model_info : S_with_collections_pretty with type t = Cil_types.model_info

module Term : S_with_collections_pretty with type t = Cil_types.term

module Term_lhost : S_with_collections_pretty with type t = Cil_types.term_lhost

module Term_offset : S_with_collections_pretty with type t = Cil_types.term_offset

module Term_lval : S_with_collections_pretty with type t = Cil_types.term_lval

module Logic_real : S_with_collections with type t = Cil_types.logic_real

module Predicate : S_with_pretty with type t = Cil_types.predicate

module Toplevel_predicate : S_with_pretty with type t = Cil_types.toplevel_predicate

module Identified_predicate : S_with_collections_pretty with type t = Cil_types.identified_predicate

module PredicateStructEq : S_with_collections with type t = Cil_types.predicate

Logic_ptree

Sorted by alphabetic order.

module Lexpr : S with type t = Logic_ptree.lexpr

Beware: no pretty-printer is available.

Frama-C API - Cil_datatype

Localisations

Cabs types

C types

ACSL types

Logic_ptree

Frama-C API - `Cil_datatype`