		Search-engine friendly clone of the ACL2 documentation.

Virtualization-for-validation

Validate-insts

Validate the model until we have done n iterations.

Signature
(validate-insts n x86) → (mv * * x86)

Definitions and Theorems

Function: validate-insts

(defun validate-insts (n x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard t))
  (let ((__function__ 'validate-insts))
    (declare (ignorable __function__))
    (b* (((when (equal n 0)) (mv t n x86))
         ((mv success? x86) (validate-inst x86))
         ((when (not success?)) (mv nil n x86)))
      (validate-insts (1- n) x86))))