• 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
            • Gcc-builtins
            • Preprocessing
            • Parsing
              • Parser
                • Parse-exprs/decls/stmts
                • Parser-states
                • Parse-external-declaration
                • Parse-cast-expression
                • Parse-expression-or-type-name
                • Parse-postfix-expression
                • Lexer
                • Parse-primary-expression
                  • Token-unary-expression-start-p
                  • Parse-declaration-specifier
                  • Parse-declaration-specifiers
                  • Parse-unary-expression-or-parenthesized-type-name
                  • Parse-asm-name-specifier
                  • Parse-specifier/qualifier
                  • Parse-expression-rest
                  • Token-type-specifier-keyword-p
                  • Parse-fileset
                  • Parse-*-external-declaration
                  • Parse-declarator-or-abstract-declarator
                  • Parse-asm-goto-labels
                  • Parse-asm-clobbers
                  • Parse-translation-unit
                  • Parse-*-label-declaration
                  • Token-postfix-expression-rest-start-p
                  • Parse-?-asm-name-specifier
                  • Parse-*-comma-identifier
                  • Parse-postfix-expression-rest
                  • Parse-expression
                  • Make-expr-unary-with-preinc/predec-ops
                  • Parse-*-stringlit
                  • Parse-statement
                  • Token-struct-declaration-start-p
                  • Parse-*-attribute-specifier
                  • Parse-initializer-list
                  • Parse-file
                  • Parse-pointer
                  • Parse-label-declaration
                  • Parse-array/function-declarator
                  • Token-type-qualifier-p
                  • Parse-*-asm-qualifier
                  • Parse-parameter-declaration
                  • Parse-attribute-name
                  • Parse-argument-expressions
                  • Make-expr-cast/add-or-cast/sub-ambig
                  • Parse-struct-or-union-specifier
                  • Parse-declaration-or-statement
                  • Parse-assignment-expression
                  • Parse-asm-clobber
                  • Token-specifier/qualifier-start-p
                  • Token-primary-expression-start-p
                  • Token-function-specifier-p
                  • Token-expression-start-p
                  • Parse-*-increment/decrement
                  • Parse-direct-abstract-declarator
                  • Parse-compound-statement
                  • Token-to-type-specifier-keyword
                  • Parse-unary-expression
                  • Parse-argument-expressions-rest
                  • Parse-generic-associations-rest
                  • Parse-conditional-expression
                  • Parse-fileset-loop
                  • Parse-direct-abstract-declarator-rest
                  • Token-designation?-initializer-start-p
                  • Token-declaration-specifier-start-p
                  • Parse-designator-list
                  • Token-abstract-declarator-start-p
                  • Parse-?-asm-output-operands
                  • Parse-?-asm-input-operands
                  • Parse-struct-declaration
                  • Parse-specifier-qualifier-list
                  • Parse-parameter-declaration-list
                  • Parse-constant-expression
                  • Token-type-specifier-start-p
                  • Token-type-qualifier-or-attribute-specifier-start-p
                  • Parse-static-assert-declaration
                  • Parse-direct-declarator
                  • Parse-declaration
                  • Parse-attribute-parameters
                  • Token-unary-operator-p
                  • Token-to-unary-operator
                  • Token-to-type-qualifier
                  • Token-storage-class-specifier-p
                  • Token-initializer-start-p
                  • Token-direct-abstract-declarator-start-p
                  • Token-declarator-start-p
                  • Parse-initializer
                  • Parse-direct-declarator-rest
                  • Token-to-storage-class-specifier
                  • Token-to-assignment-operator
                  • Token-to-asm-qualifier
                  • Token-struct-declarator-start-p
                  • Token-direct-declarator-start-p
                  • Token-assignment-operator-p
                  • Parse-type-qualifier-and-attribute-specifier-list
                  • Parse-enumerator-list
                  • Parse-designation?-initializer
                  • Parse-compound-literal
                  • Parse-block-item
                  • Token-type-name-start-p
                  • Token-to-function-specifier
                  • Token-preinc/predec-operator-p
                  • Token-multiplicative-operator-p
                  • Token-designator-start-p
                  • Token-designation-start-p
                  • Parse-generic-association
                  • Parse-declaration-list
                  • Parse-attribute-specifier
                  • Parse-asm-output-operands
                  • Token-to-relational-operator
                  • Token-to-preinc/predec-operator
                  • Token-to-multiplicative-operator
                  • Token-relational-operator-p
                  • Token-equality-operator-p
                  • Token-asm-qualifier-p
                  • Token-additive-operator-p
                  • Parse-asm-statement
                  • Parse-asm-input-operands
                  • Token-to-equality-operator
                  • Token-to-additive-operator
                  • Token-shift-operator-p
                  • Parser-messages
                  • Parse-type-name
                  • Parse-struct-declarator-list
                  • Parse-struct-declaration-list
                  • Parse-relational-expression-rest
                  • Parse-multiplicative-expression-rest
                  • Parse-logical-or-expression-rest
                  • Parse-logical-and-expression-rest
                  • Parse-inclusive-or-expression-rest
                  • Parse-exclusive-or-expression-rest
                  • Parse-equality-expression-rest
                  • Parse-array/function-abstract-declarator
                  • Parse-additive-expression-rest
                  • Token-to-shift-operator
                  • Parse-struct-declarator
                  • Parse-shift-expression-rest
                  • Parse-member-designor
                  • Parse-init-declarator-list
                  • Parse-init-declarator
                  • Parse-designator
                  • Parse-and-expression-rest
                  • Parse-alignment-specifier
                  • Reader
                  • Parse-shift-expression
                  • Parse-relational-expression
                  • Parse-multiplicative-expression
                  • Parse-logical-or-expression
                  • Parse-logical-and-expression
                  • Parse-inclusive-or-expression
                  • Parse-exclusive-or-expression
                  • Parse-equality-expression
                  • Parse-enum-specifier
                  • Parse-block-item-list
                  • Parse-attribute-list
                  • Parse-and-expression
                  • Parse-additive-expression
                  • Parse-abstract-declarator
                  • Parse-member-designor-rest
                  • Parse-declarator
                  • Parse-attribute
                  • Parse-type-qualifier-or-attribute-specifier
                  • Parse-enumerator
                  • Parse-asm-output-operand
                  • Parse-asm-input-operand
            • 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
    • Parser
    • Parse-exprs/decls/stmts

    Parse-primary-expression

    Parse a primary expression.

    Signature
    (parse-primary-expression parstate) 
      → 
    (mv erp expr span new-parstate)
    Arguments
    parstate — Guard (parstatep parstate).
    Returns
    expr — Type (exprp expr).
    span — Type (spanp span).
    new-parstate — Type (parstatep new-parstate), given (parstatep parstate).

    This is called when we expect an expression.

    We read a token.

    If the token is an identifier or a constant, that is the whole expression.

    If the token is a string literal, we read zero or more that may follow, and we have a string literal expression. Recall that C supports automatically concatenated adjacent string literals, and that our abstract syntax preserves the distinct string literals.

    If the token is an open parenthesis, we read another token to see whether it is an open curly brace. If it is, we have a statement expression (a GCC extension); otherwise, we have a parenthesized expression. We only allow this if GCC extensions are supported.

    If the token is the keyword _Generic, we parse an open parenthesis and an assignment expression, then a comma and a generic association, since there must be at least one. Then we call a separate function to parse zero or more additional generic associations. Finally we parse a closed parenthesis and return a generic selection.

    If the token is the GCC keyword __builtin_types_compatible_p, we parse a call of this built-in function, which has two type names as arguments.

    If the token is the GCC keyword __builtin_offsetof, we parse a call of this built-in function, which has a type name and a member designator as arguments.

    If the token is the GCC keyword __builtin_va_arg, we parse a call of this built-in function, which has an expression and a type name as arguments.

    If the token is the GCC keyword __extension__, we parse the primary expression after it, recursively.

    If the token is none of the above, including the token being absent, it is an error.

    We temporarily allow true and false as synonyms of the expressions (constants) 1 and 0. We plan to parameterize this and other functions over the specific C version, including choice of GCC extensions.