		Search-engine friendly clone of the ACL2 documentation.

Parser

Parse-translation-unit

Parse a translation unit.

Signature
(parse-translation-unit parstate) → (mv erp tunit new-parstate)
Arguments: parstate — Guard (parstatep parstate).
Returns: tunit — Type (transunitp tunit).; new-parstate — Type (parstatep new-parstate), given (parstatep parstate).

This is called, by parse-file, on the initial parsing state, which contains all the file data bytes. We parse zero or more external declarations, consistently with the grammar. But unless GCC extensions are enabled, we reject input with zero external declarations.

We also ensure that the file ends in new-line, as prescribed in [C17:5.1.1.2/1/2]. We check that the end-of-file position, returned by parse-*-external-declaration, is at column 0: this means that, since the file is not empty, the last character is a new-line, otherwise that position would be at a non-zero column.

Definitions and Theorems

Function: parse-translation-unit

(defun parse-translation-unit (parstate)
 (declare (xargs :stobjs (parstate)))
 (declare (xargs :guard (parstatep parstate)))
 (let ((__function__ 'parse-translation-unit))
  (declare (ignorable __function__))
  (b*
   (((reterr) (irr-transunit) parstate)
    ((erp extdecls & eof-pos parstate)
     (parse-*-external-declaration parstate))
    ((when (and (endp extdecls)
                (not (parstate->gcc parstate))))
     (reterr
      (msg
       "The translation unit has no external declarations, ~
                      but GCC extensions (which allow that) are not enabled.")))
    ((unless (= (position->column eof-pos) 0))
     (reterr (msg "The file does not end in new-line."))))
   (retok (make-transunit :declons extdecls
                          :info nil)
          parstate))))

Theorem: transunitp-of-parse-translation-unit.tunit

(defthm transunitp-of-parse-translation-unit.tunit
  (b* (((mv acl2::?erp ?tunit ?new-parstate)
        (parse-translation-unit parstate)))
    (transunitp tunit))
  :rule-classes :rewrite)

Theorem: parstatep-of-parse-translation-unit.new-parstate

(defthm parstatep-of-parse-translation-unit.new-parstate
  (implies (parstatep parstate)
           (b* (((mv acl2::?erp ?tunit ?new-parstate)
                 (parse-translation-unit parstate)))
             (parstatep new-parstate)))
  :rule-classes :rewrite)

Theorem: parsize-of-parse-translation-unit-uncond

(defthm parsize-of-parse-translation-unit-uncond
  (b* (((mv acl2::?erp ?tunit ?new-parstate)
        (parse-translation-unit parstate)))
    (<= (parsize new-parstate)
        (parsize parstate)))
  :rule-classes :linear)