		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)