		Search-engine friendly clone of the ACL2 documentation.

Atj-java-primitive-array-model

Byte-array-length

Obtain the length of a Java byte array.

Signature
(byte-array-length array) → length
Arguments: array — Guard (byte-arrayp array).
Returns: length — Type (int-valuep length).

Definitions and Theorems

Function: byte-array-length

(defun byte-array-length (array)
  (declare (xargs :guard (byte-arrayp array)))
  (let ((__function__ 'byte-array-length))
    (declare (ignorable __function__))
    (int-value (len (byte-array->components array)))))

Theorem: int-valuep-of-byte-array-length

(defthm int-valuep-of-byte-array-length
  (b* ((length (byte-array-length array)))
    (int-valuep length))
  :rule-classes :rewrite)