		Search-engine friendly clone of the ACL2 documentation.

Virtualization-for-validation

Run-until-rip-or-n

Execute the model until we reach the given rip address or have executed n instructions.

Signature
(run-until-rip-or-n rip n x86) → (mv * x86)

Definitions and Theorems

Function: run-until-rip-or-n

(defun run-until-rip-or-n (rip n x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard t))
  (let ((__function__ 'run-until-rip-or-n))
    (declare (ignorable __function__))
    (if (or (= n 0)
            (ms x86)
            (fault x86)
            (equal (rip x86) (i64 rip)))
        (mv (equal (rip x86) (i64 rip)) x86)
      (b* ((x86 (x86-fetch-decode-execute x86)))
        (run-until-rip-or-n rip (1- n) x86)))))