		Search-engine friendly clone of the ACL2 documentation.

Elf-reader

Elf-read-string-null-term

Read a null terminated string from a given offset of byte-list

Signature
(elf-read-string-null-term byte-list offset) → str
Arguments: byte-list — Guard (byte-listp byte-list).; offset — Guard (natp offset).
Returns: str — Type (stringp str).

Definitions and Theorems

Function: elf-read-string-null-term

(defun elf-read-string-null-term (byte-list offset)
  (declare (xargs :guard (and (byte-listp byte-list)
                              (natp offset))))
  (declare (xargs :guard (<= offset (len byte-list))))
  (let ((__function__ 'elf-read-string-null-term))
    (declare (ignorable __function__))
    (let* ((bytes (elf-read-mem-null-term byte-list offset))
           (charlist (bytes->charlist bytes)))
      (coerce charlist 'string))))

Theorem: stringp-of-elf-read-string-null-term

(defthm stringp-of-elf-read-string-null-term
  (b* ((str (elf-read-string-null-term byte-list offset)))
    (stringp str))
  :rule-classes :type-prescription)