Check-fib-output
- Signature
(check-fib-output input halt-address x86) → *
- Arguments
- x86 — Output x86 State.
Definitions and Theorems
Function: check-fib-output
(defun
check-fib-output
(input halt-address x86)
(declare (xargs :stobjs (x86)))
(declare (type (unsigned-byte 50) input)
(type (signed-byte 48) halt-address))
(let
((__function__ 'check-fib-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 (fib input)))
(cond
((equal (rgfi *rax* x86) expected)
(prog2$
(cw "~|(x86isa-fib ~x0) was correctly computed as ~x1.~%"
input expected)
t))
(t (prog2$ (cw "~|(x86isa-fib ~x0) = ~x1, but rax is ~x2.~%"
input expected (rgfi *rax* x86))
t))))))))
