• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • C
          • Syntax-for-tools
            • Formalized-subset
            • Mapping-to-language-definition
            • Input-files
            • Compilation-database
            • Printer
            • Output-files
            • Abstract-syntax-operations
            • Implementation-environments
            • Abstract-syntax
            • Concrete-syntax
            • Disambiguation
            • Validation
              • Validator
              • Validation-information
                • Abstract-syntax-annop
                • Types
                  • Type-compatiblep
                  • Type-uaconvert-signed-unsigned
                  • Type-uaconvert
                  • Type-integer-promote
                  • Type-params-compatiblep
                  • Type-option
                  • Type-formalp
                  • Ldm-type
                  • Make-pointers-to
                  • Type-list-default-arg-promote
                  • Type-uaconvert-unsigned
                  • Type-uaconvert-signed
                  • Type-default-arg-promote
                  • Type-default-arg-promotedp
                  • Type-params-composite
                  • Type-integer-promotedp
                  • Ldm-type-option-set
                  • Type-unsigned-integerp
                  • Type-standard-unsigned-integerp
                  • Type-signed-integerp
                  • Type-to-value-kind
                  • Type-standard-signed-integerp
                  • Ildm-type
                  • Type-arithmeticp
                  • Ldm-type-set
                  • Ldm-type-option
                  • Type-standard-integerp
                  • Type-option-set-formalp
                  • Type-real-floatingp
                  • Type-option-formalp
                  • Type-integerp
                  • Type-characterp
                  • Type-basicp
                  • Type-aggregatep
                  • Type-scalarp
                  • Type-realp
                  • Type-fpconvert
                  • Type-floatingp
                  • Type-complexp
                  • Type-set-formalp
                  • Type-apconvert
                  • Type-composite
                  • Ident-type-map
                  • Type-set
                  • Type-option-type-alist
                  • Type-option-set
                  • Type-list-compatiblep
                  • Irr-type-params
                  • Irr-type
                  • Type-list-composite
                  • Type/type-params/type-list
                    • Type
                      • Typep
                      • Type-case
                      • Type-kind
                      • Type-equiv
                      • Type-function
                      • Type-struct
                      • Type-pointer
                      • Type-array
                      • Type-void
                      • Type-ushort
                      • Type-unknown
                      • Type-union
                      • Type-ulong
                      • Type-ullong
                      • Type-uint
                      • Type-uchar
                      • Type-sshort
                      • Type-slong
                      • Type-sllong
                      • Type-sint
                      • Type-schar
                      • Type-ldoublec
                      • Type-ldouble
                      • Type-floatc
                      • Type-float
                      • Type-enum
                      • Type-doublec
                      • Type-double
                      • Type-char
                      • Type-bool
                      • Type-fix
                      • Type-count
                    • Type-params
                    • Type-list
                • Abstract-syntax-anno-additional-theroems
                • Valid-ext-info
                • Valid-table
                • Valid-ord-info
                • Uid
                • Stmts-types
                • Lifetime
                • Init-declor-info
                • Fundef-types
                • Expr-type
                • Valid-defstatus
                • Var-info
                • Valid-ord-info-option
                • Valid-ext-info-option
                • Uid-option
                • Linkage-option
                • Linkage
                • Lifetime-option
                • Valid-table-option
                • Iconst-info
                • Param-declor-nonabstract-info
                • Fundef-info
                • Expr-null-pointer-constp
                • Valid-scope
                • Const-expr-null-pointer-constp
                • Expr-string-info
                • Expr-funcall-info
                • Expr-arrsub-info
                • Tyname-info
                • Transunit-info
                • Expr-unary-info
                • Expr-const-info
                • Expr-binary-info
                • Stmt-types
                • Block-item-list-types
                • Initer-type
                • Valid-ord-scope
                • Uid-increment
                • Uid-equal
                • Coerce-var-info
                • Valid-externals
                • Irr-var-info
                • Valid-scope-list
                • Irr-valid-table
                • Irr-lifetime
                • Irr-uid
                • Irr-linkage
                • Block-item-types
                • Comp-stmt-types
            • Gcc-builtins
            • Preprocessing
            • Parsing
          • Atc
          • Transformation-tools
          • Language
          • Representation
          • Insertion-sort
          • Pack
        • Soft
        • Bv
        • Imp-language
        • Ethereum
        • Event-macros
        • Java
        • Riscv
        • Bitcoin
        • Zcash
        • Yul
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
        • File-io-light
        • Cryptography
        • Number-theory
        • Axe
        • Lists-light
        • Builtins
        • Solidity
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Type/type-params/type-list

Type

Fixtype of C types [C17:6.2.5].

This is a tagged union type, introduced by fty::deftagsum.

Member Tags → Types
:void → type-void
:char → type-char
:schar → type-schar
:uchar → type-uchar
:sshort → type-sshort
:ushort → type-ushort
:sint → type-sint
:uint → type-uint
:slong → type-slong
:ulong → type-ulong
:sllong → type-sllong
:ullong → type-ullong
:float → type-float
:double → type-double
:ldouble → type-ldouble
:floatc → type-floatc
:doublec → type-doublec
:ldoublec → type-ldoublec
:bool → type-bool
:struct → type-struct
:union → type-union
:enum → type-enum
:array → type-array
:pointer → type-pointer
:function → type-function
:unknown → type-unknown

Currently we do not model all the C types in detail, but only an approximate version of them, which still lets us perform some validation. We plan to refine the types, and the rest of the validator, to cover exactly all the validity checks prescribed by [C17] (as well as applicable GCC extensions).

We capture the following types:

  • The void type [C17:6.2.5/19].
  • The plain char type [C17:6.2.5/3].
  • The five standard signed integer types [C17:6.2.5/4] and the corresponding unsigned integer types [C17:6.2.5/6].
  • The three real floating point types [C17:6.2.5/10].
  • The three complex types [C17:6.2.5/11]. These are a conditional feature, but they must be included in this fixtype because this fixtype consists of all the possible types.
  • The _Bool type [C17:6.2.5/2].
  • A family of structure types [C17:6.2.5/20]. Structure types are characterized by an optional tag. This is an approximation, because there may be different structure types of a given tag, or different tagless structure types.
  • A collective type for all union types [C17:6.2.5/20]. This is an approximation, because there are different union types.
  • A collective type for all enumeration types [C17:6.2.5/20]. This is an approximation, because there are different enumeration types.
  • An array type [C17:6.2.5/20], derived from the ``element type.'' This is an approximation, because we do not track the size of the array type.
  • A pointer type [C17:6.2.5/20], derived from the ``referenced type.''
  • A function type [C17:6.2.5/20], which contains the return type and parameter information (see type-params).
  • An ``unknown'' type that we need due to our current approximation. Our validator must not reject valid code. But due to our approximate treatment of types, we cannot always calculate a type, e.g. for a member expression of the form s.m where s is an expression with structure type. Since our approximate type for all structure types has no information about the members, we cannot calculate any actual type for s.m; but if the expression is used elsewhere, we need to accept it, because it could have the right type. We use this unknown type for this purpose: the expression s.m has unknown type, and unknown types are always acceptable.

Besides the approximations noted above, currently we do not capture atomic types [C17:6.2.5/20], which we approximate as the underlying (argument) type. We also do not capture typedef names, which are instead expanded to their normal form. Furthermore, we do not capture qualified types [C17:6.2.5/26].

Subtopics

Typep
Recognizer for type structures.
Type-case
Case macro for the different kinds of type structures.
Type-kind
Get the kind (tag) of a type structure.
Type-equiv
Basic equivalence relation for type structures.
Type-function
Type-struct
Type-pointer
Type-array
Type-void
Type-ushort
Type-unknown
Type-union
Type-ulong
Type-ullong
Type-uint
Type-uchar
Type-sshort
Type-slong
Type-sllong
Type-sint
Type-schar
Type-ldoublec
Type-ldouble
Type-floatc
Type-float
Type-enum
Type-doublec
Type-double
Type-char
Type-bool
Type-fix
Fixing function for type structures.
Type-count
Measure for recurring over type structures.