		Search-engine friendly clone of the ACL2 documentation.

Jenkins-hash

Jenkins-acc-string

Signature
(jenkins-acc-string str acc) → acc$
Returns: acc$ — Type (unsigned-byte-p 32 acc$).

Definitions and Theorems

Function: jenkins-acc-string$inline

(defun jenkins-acc-string$inline (str acc)
 (declare
      (type string str)
      (type (unsigned-byte 32) acc)
      (xargs :type-prescription (natp (jenkins-acc-string str acc)))
      (optimize (speed 3) (safety 0)))
 (declare (xargs :guard t))
 (the (unsigned-byte 32)
      (let ((len (length str)))
        (declare (type unsigned-byte len))
        (if (<= len *u-fixnum-max*)
            (jenkins-acc-string-fixnum-index
                 str 0 (the (unsigned-byte 61) len)
                 acc)
          (jenkins-acc-string-nonfixnum-index str 0 len acc)))))

Theorem: return-type-of-jenkins-acc-string

(defthm return-type-of-jenkins-acc-string
  (b* ((acc$ (jenkins-acc-string$inline str acc)))
    (unsigned-byte-p 32 acc$))
  :rule-classes :rewrite)