		Search-engine friendly clone of the ACL2 documentation.

Elf-reader

Elf-read-mem-null-term

Read a location at an offset of a given byte-list and return the list of bytes until a null is encountered (null not included)

Signature
(elf-read-mem-null-term byte-list offset) → bl
Arguments: byte-list — Guard (byte-listp byte-list).; offset — Guard (natp offset).
Returns: bl — Type (byte-listp bl), given (and (natp offset) (byte-listp byte-list)).

Definitions and Theorems

Function: elf-read-mem-null-term

(defun elf-read-mem-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-mem-null-term))
   (declare (ignorable __function__))
   (if
     (natp offset)
     (if (< offset (len byte-list))
         (let* ((val (car (nthcdr offset byte-list))))
           (if (equal 0 val)
               nil
             (cons val
                   (elf-read-mem-null-term byte-list (1+ offset)))))
       nil)
     nil)))

Theorem: byte-listp-of-elf-read-mem-null-term

(defthm byte-listp-of-elf-read-mem-null-term
  (implies (and (natp offset)
                (byte-listp byte-list))
           (b* ((bl (elf-read-mem-null-term byte-list offset)))
             (byte-listp bl)))
  :rule-classes :rewrite)