Parse (the data bytes of) a file.
(parse-file path data gcc) → (mv erp tunit)
We also pass a flag saying whether GCC extensions should be accepted.
If successful, the result is a translation unit. We initialize the parser state with the data bytes, and we attempt to parse them as a translation unit. The final parser state is discarded, since it is no longer needed.
If an error occurs, we enhance it with
information about the file path.
It is the case that
Function:
(defun parse-file (path data gcc) (declare (xargs :guard (and (filepathp path) (byte-listp data) (booleanp gcc)))) (let ((__function__ 'parse-file)) (declare (ignorable __function__)) (b* (((reterr) (irr-transunit)) (parstate (init-parstate data gcc)) ((mv erp tunit &) (parse-translation-unit parstate)) ((when erp) (b* (((unless (msgp erp)) (raise "Internal error: ~x0 is not a message." erp) (reterr t))) (reterr (msg "Error in file ~x0: ~@1" (filepath->unwrap path) erp))))) (retok tunit))))
Theorem:
(defthm transunitp-of-parse-file.tunit (b* (((mv acl2::?erp ?tunit) (parse-file path data gcc))) (transunitp tunit)) :rule-classes :rewrite)