Check-fib32-output
- Signature
(check-fib32-output input halt-address x86) → *
- Arguments
- x86 — Output x86 State.
Definitions and Theorems
Function: check-fib32-output
(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))))))))
