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