[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] type-error in KERNEL

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.


134218304 is not of type (UNSIGNED-BYTE 27)

[condition of type TYPE-ERROR]



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,