File-length$
The size of a file in bytes
This analogue of the Common Lisp function, file-length, uses
that function under the hood to compute efficiently the number of bytes B
in the specified file if that number can be determined, returning (mv B
state); otherwise it returns (mv nil state). The guard of
file-length$ requires that the first argument is a string; the second
argument is the ACL2 state. The logical definition does not actually
look at the file and hence is not useful for reasoning about the number of
bytes in the file.
Function: file-length$
(defun file-length$ (file state)
(declare (xargs :guard (stringp file)
:stobjs state))
(declare (ignore file))
(mv-let (erp val state)
(read-acl2-oracle state)
(mv (and (null erp) (natp val) val)
state)))
