Re: [PVS-Help] type-error in KERNEL

[Sam Owre <owre@xxxxxxxxxxx>]

Hi Yunja,

>From the message, I see you're using CMU Lisp, and my first
guess is that the pvs-sxhash function (defined in
src/utils/hashfn.lisp) is returning a value that's out of
range, and the hash functions that use this are complaining.
Keep in mind this is a guess, you need to get a backtrace and
do some detective work to chase it down.

I'll be happy to take a look at it, if you don't mind sending
me your specs and instructions for recreating the bug.

Regards,
Sam Owre


최윤자 <yuchoi76@knu.ac.kr> wrote:

> X-RCPTTO: pvs-help@csl.sri.com
> x-beehive-trace: yuchoi76@knu.ac.kr pvs-help@csl.sri.com 155.230.105.127
> x-beehive-kind: normal
> x-beehive-modified: received kind
> From: 최윤자 <yuchoi76@knu.ac.kr>
> To: <pvs-help@csl.sri.com>
> Date: Fri, 21 Dec 2007 20:11:26 +0900
> Organization: 전자전기컴퓨터학부
> X-Mailer: Microsoft Office Outlook, Build 11.0.5510
> X-SRI-Archive: pvs-help
> Subject: [PVS-Help] type-error in KERNEL
> Sender: pvs-help-bounces+owre=csl.sri.com@csl.sri.com
> 
> 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