• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Soft
      • Bv
      • Imp-language
      • C
        • Syntax-for-tools
          • Disambiguator
          • Abstract-syntax
          • Parser
            • Parse-exprs/decls/stmts
            • Check-full-ppnumber
            • Read-char
            • Parstate
            • Lex-identifier/keyword
            • Lex-oct-iconst-/-dec-fconst
            • Lex-lexeme
            • Parse-external-declaration
            • Parse-cast-expression
            • Lex-isuffix-if-present
            • Parse-expression-or-type-name
            • Parse-postfix-expression
            • Lex-hex-iconst/fconst
            • Lex-dec-iconst/fconst
            • Lex-block-comment
            • Lex-escape-sequence
            • Read-token
            • Token
            • Lex-*-hexadecimal-digit
            • Lex-*-c-char
            • Lex-*-s-char
            • Parse-specifier/qualifier
            • Lex-*-digit
            • Lex-line-comment
            • Char-to-msg
            • Parse-primary-expression
            • Parse-declaration-specifier
            • Lex-iconst/fconst
            • Parse-external-declaration-list
            • Parse-declaration-specifiers
            • Lex-dec-expo-if-present
            • Init-parstate
            • Reread-to-token
            • Parse-asm-name-specifier
            • Lex-character-constant
            • Parse-expression-rest
            • Parstate$
            • Lex-dec-fconst
            • Token-unary-expression-start-p
            • Parse-declarator-or-abstract-declarator
            • Parse-asm-goto-labels
            • Parse-asm-clobbers
            • Lex-stringlit
            • Lex-non-octal-digit
            • Position
            • Lexeme
            • Lex-fsuffix-if-present
            • Lex-hexadecimal-digit
            • Token-type-specifier-keyword-p
            • Parse-translation-unit
            • Token-postfix-expression-rest-start-p
            • To-parstate$
            • Parse-?-asm-name-specifier
            • Parse-postfix-expression-rest
            • Parse-expression
            • Lex-sign-if-present
            • Lex-dec-expo
            • Lex-bin-expo
            • Unread-to-token
            • Parse-*-stringlit
            • Parse-statement
            • Parse-fileset
            • Make-expr-unary-with-preinc/predec-ops
            • Token-option
            • Lexeme-option
            • Token-struct-declaration-start-p
            • Parse-*-attribute-specifier
            • Parse-initializer-list
            • Parse-file
            • Parse-pointer
            • Parse-array/function-declarator
            • Unread-chars
            • Span
            • Read-stringlit
            • Lex-hex-quad
            • Unread-tokens
            • Token-type-qualifier-p
            • Read-identifier
            • Parse-*-asm-qualifier
            • Unread-char
            • Parse-attribute-name
            • Parse-argument-expressions
            • Make-expr-cast/add-or-cast/sub-ambig
            • Read-punctuator
            • Parse-struct-or-union-specifier
            • Parse-assignment-expression
            • Parse-asm-clobber
            • Token-specifier/qualifier-start-p
            • Token-primary-expression-start-p
            • Token-function-specifier-p
            • Reterr-msg
            • Read-keyword
            • Parse-*-increment/decrement
            • Parse-direct-abstract-declarator
            • Parse-declaration-or-statement
            • Char+position
            • Unread-token
            • Token+span
            • Token-expression-start-p
            • Update-parstate->tokens-unread
            • Update-parstate->chars-unread
            • Token-to-msg
            • Update-parstate->tokens-read
            • Update-parstate->tokens-length
            • Update-parstate->position
            • Update-parstate->chars-read
            • Parse-parameter-declaration
            • Parse-argument-expressions-rest
            • Update-parstate->chars-length
            • Token-to-type-specifier-keyword
            • Update-parstate->bytes
            • Parse-unary-expression
            • Parse-generic-associations-rest
            • Parse-conditional-expression
            • Update-parstate->size
            • Update-parstate->gcc
            • Parsize
            • Parse-direct-abstract-declarator-rest
            • Token-declaration-specifier-start-p
            • Parse-designator-list
            • Token-designation?-initializer-start-p
            • 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-fileset-loop
            • 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-punctuatorp
            • Token-direct-abstract-declarator-start-p
            • Token-declarator-start-p
            • Parse-direct-declarator-rest
            • Token-to-storage-class-specifier
            • Token-to-assignment-operator
            • Token-to-asm-qualifier
            • Token-struct-declarator-start-p
            • Token-keywordp
            • Token-initializer-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
            • Parstate->tokens-unread
            • Parstate->chars-unread
            • Parstate->bytes
            • Parse-initializer
            • 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
            • Span-join
            • Parstate->tokens-read
            • Parstate->tokens-length
            • Parstate->size
            • Parstate->chars-read
            • Parstate->chars-length
            • Parse-asm-statement
            • Parse-asm-input-operands
            • Update-parstate->token
            • Update-parstate->char
            • Token-to-equality-operator
            • Token-to-additive-operator
            • Token-shift-operator-p
            • To-parstate$-tokens-unread
            • To-parstate$-chars-unread
            • Position-inc-line
            • Position-inc-column
            • Parstate->gcc
            • 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
            • To-parstate$-tokens-read
            • Parse-struct-declarator
            • Parse-shift-expression-rest
            • Parse-member-designor
            • Parse-init-declarator-list
            • Parse-init-declarator
            • Parse-and-expression-rest
            • Parse-alignment-specifier
            • To-parstate$-chars-read
            • Position-to-msg
            • Parstate->token
            • Parstate->char
            • 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
            • Char+position-list
            • Token+span-list
            • Span-to-msg
            • Parstate-fix
            • Parse-member-designor-rest
            • Position-init
            • Parstate->position
            • Parse-designator
            • Parse-declarator
            • Parse-attribute
            • Irr-token
            • Irr-span
            • Irr-position
            • Irr-lexeme
            • Token-list
            • Parse-type-qualifier-or-attribute-specifier
            • Parse-enumerator
            • Parse-asm-output-operand
            • Parse-asm-input-operand
          • Validator
          • Printer
          • Formalized-subset
          • Mapping-to-language-definition
          • Defpred
          • Output-files
          • Input-files
          • Abstract-syntax-operations
          • Implementation-environments
          • Concrete-syntax
          • Unambiguity
          • Preprocessing
          • Abstraction-mapping
          • Annotation
        • Atc
        • Language
        • Representation
        • Transformation-tools
        • Pack
      • Event-macros
      • Java
      • Bitcoin
      • Ethereum
      • Yul
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Number-theory
      • Cryptography
      • Lists-light
      • Builtins
      • Axe
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Parser

Lex-iconst/fconst

Lex an integer or floating constant.

Signature

(lex-iconst/fconst first-digit first-pos parstate) 
  → 
(mv erp const last-pos new-parstate)

Arguments

first-digit — Guard (dec-digit-char-p first-digit).

first-pos — Guard (positionp first-pos).

parstate — Guard (parstatep parstate).

Returns

const — Type (constp const).

last-pos — Type (positionp last-pos).

new-parstate — Type (parstatep new-parstate), given (parstatep parstate).

This is called when we expect an integer or floating constant, after reading the first (decimal) digit of the constant. The first digit and its position are passed to this function.

If the first digit is a 0, we check the next character. If there is no next character, we have the octal constant 0. If instead the next character is x or X, we must have a hexadecimal constant, for which we call a separate function. If instead the next character is something else, we must have an octal integer or decimal floating constant: we put back the character and call a separate function.

If instead the first digit is 1 to 9, we must have a decimal integer or floating constant, for which we use a separate function.

Definitions and Theorems

Function: lex-iconst/fconst

(defun lex-iconst/fconst (first-digit first-pos parstate)
 (declare (xargs :stobjs (parstate)))
 (declare (xargs :guard (and (dec-digit-char-p first-digit)
                             (positionp first-pos)
                             (parstatep parstate))))
 (let ((__function__ 'lex-iconst/fconst))
  (declare (ignorable __function__))
  (b* (((reterr)
        (irr-const)
        (irr-position)
        parstate))
   (cond
    ((eql first-digit #\0)
     (b* (((erp char pos parstate)
           (read-char parstate)))
      (cond
       ((not char)
        (retok
         (const-int
             (make-iconst
                  :core (make-dec/oct/hex-const-oct :leading-zeros 1
                                                    :value 0)
                  :suffix? nil))
         (position-fix first-pos)
         parstate))
       ((or (= char (char-code #\x))
            (= char (char-code #\X)))
        (b* ((hprefix (if (= char (char-code #\x))
                          (hprefix-locase-0x)
                        (hprefix-upcase-0x))))
          (lex-hex-iconst/fconst hprefix pos parstate)))
       (t (b* ((parstate (unread-char parstate)))
            (lex-oct-iconst-/-dec-fconst first-pos parstate))))))
    (t (lex-dec-iconst/fconst first-digit first-pos parstate))))))

Theorem: constp-of-lex-iconst/fconst.const

(defthm constp-of-lex-iconst/fconst.const
  (b* (((mv acl2::?erp
            ?const ?last-pos ?new-parstate)
        (lex-iconst/fconst first-digit first-pos parstate)))
    (constp const))
  :rule-classes :rewrite)

Theorem: positionp-of-lex-iconst/fconst.last-pos

(defthm positionp-of-lex-iconst/fconst.last-pos
  (b* (((mv acl2::?erp
            ?const ?last-pos ?new-parstate)
        (lex-iconst/fconst first-digit first-pos parstate)))
    (positionp last-pos))
  :rule-classes :rewrite)

Theorem: parstatep-of-lex-iconst/fconst.new-parstate

(defthm parstatep-of-lex-iconst/fconst.new-parstate
 (implies (parstatep parstate)
          (b* (((mv acl2::?erp
                    ?const ?last-pos ?new-parstate)
                (lex-iconst/fconst first-digit first-pos parstate)))
            (parstatep new-parstate)))
 :rule-classes :rewrite)

Theorem: parsize-of-lex-iconst/fconst-uncond

(defthm parsize-of-lex-iconst/fconst-uncond
  (b* (((mv acl2::?erp
            ?const ?last-pos ?new-parstate)
        (lex-iconst/fconst first-digit first-pos parstate)))
    (<= (parsize new-parstate)
        (parsize parstate)))
  :rule-classes :linear)