Run-x86isa-fib
- Signature
(run-x86isa-fib input start-address
halt-address xrun-limit sys-view? x86)
→
(mv * * x86)- Arguments
- sys-view? — Guard (booleanp sys-view?).
Definitions and Theorems
Function: run-x86isa-fib
(defun run-x86isa-fib (input start-address
halt-address xrun-limit sys-view? x86)
(declare (xargs :stobjs (x86)))
(declare (type (unsigned-byte 50) input)
(type (signed-byte 48) start-address)
(type (signed-byte 48) halt-address)
(type (unsigned-byte 50) xrun-limit))
(declare (xargs :guard (booleanp sys-view?)))
(let ((__function__ 'run-x86isa-fib))
(declare (ignorable __function__))
(if (zp input)
(mv t 0 x86)
(b*
(((mv flg steps x86)
(x86isa-one-fib-cosim (1- input)
start-address
halt-address xrun-limit sys-view? x86))
((unless flg)
(cw "~% Mismatch found!~%")
(mv flg steps x86)))
(run-x86isa-fib (1- input)
start-address halt-address
xrun-limit sys-view? x86)))))
