		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)