|
Hi everyone, I am new to PVS (and new to LISP, too). While trying to prove a PVS
model I wrote, I have encountered the following type-error. Type-error in KERNEL : OBJECT-NOT-FOUND-ERROR-HANDLER 134218304 is not of type (UNSIGNED-BYTE 27) [condition of type
TYPE-ERROR] Restarts: After the error message, the checking process continues for a
while until the prover generates a long warning message and takes an abnormal
stop. Briefly speaking, the warning message says pvs-undo-info is
discarded since it exceeds the limit. My best guess is that some of the recursive functions generate a
mismatched-type value as a parameter to themselves. I interpreted the message as ¡°one of the recursive calls generate 134218304
which is out-of-range for unsigned-byte¡±, out of pure guesswork. I have been trying to locate the source of the error for a
while without a success since my recursive functions do not increase parameter
values. Therefore, I would like to confirm with experts that I am
digging into the right direction. Can somebody interpret the exact meaning of this error message
for me? Can this type-error cause an abnormal stop even though the
prover continues after the error occurs? Many thanks in advance, Yunja |