(check-fib32-output input halt-address x86) → *
Function:
(defun check-fib32-output (input halt-address x86) (declare (xargs :stobjs (x86))) (declare (type (unsigned-byte 8) input) (type (signed-byte 48) halt-address)) (let ((__function__ 'check-fib32-output)) (declare (ignorable __function__)) (cond ((or (fault x86) (not (equal (ms x86) (cons (cons 'x86-fetch-decode-execute-halt (cons ':rip (cons halt-address 'nil))) 'nil)))) (cw "~|(ms x86) = ~x0 (fault x86) = ~x1~%" (ms x86) (fault x86))) (t (let ((expected (fib32 input))) (cond ((equal (rgfi *eax* x86) expected) (prog2$ (cw "~|(x86isa-fib ~x0) was correctly computed as ~x1.~%" input expected) t)) (t (prog2$ (cw "~|(x86isa-fib ~x0) = ~x1, but eax is ~x2.~%" input expected (rgfi *eax* x86)) t))))))))