Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

PVS Bug 632


Synopsis:        errors with records
Severity:        serious
Priority:        medium
Responsible:     owre
State:           analyzed
Class:           sw-bug
Arrival-Date:    Tue Dec 11 16:55:01 2001
Originator:      Jaco van de Pol
Organization:    cwi.nl
Release:         PVS 2.4
Environment: 
 System:          
 Architecture: 

Description: 
  This is a multipart MIME message.
  
  --==_Exmh_5309712040
  Content-Type: text/plain; charset=us-ascii
  
  Hi,
  
  When redoing some proofs in pvs 2.4 I found an error.
  One occurred when typechecking the first file (attached below).
  typechecking it in pvs 2.4 on a Linux machine yields:
  
     Error: Received signal number 4 (Illegal instruction)
  
  (or sometimes I get the error:
     Error: Attempt to take the cdr of -532124669 which is not listp.
  )
  
  Now replacing the second "emptyset" by "emptyset[DataItems]" helps: 
  the system typechecks again.
  
  Next, I call the prover on the lemma.
  Then (rewrite "sp") (assert) gives the following error:
  
  Error: Recursive error while printing or signalling an error.  This is
         sometimes caused by an error in a print-object method.
  
  (or sometimes I got the message:
  Error: Attempt to take the cdr of #1\%bell which is not listp.
    [condition type: SIMPLE-ERROR]
  )
  
  Hope the bug-report is clear enough.
  Kind regards,
  Jaco van de Pol.
  
  
  
  --==_Exmh_5309712040
  Content-Type: text/plain ; name="error.pvs"; charset=us-ascii
  Content-Description: error.pvs
  Content-Disposition: attachment; filename="error.pvs"
  
  error: THEORY
  
  BEGIN
  
  DataItems : TYPE = [# data : nat, timestamp : real #]
  WriteSets: TYPE = setof[DataItems]
  
  
  SemPrim : TYPE = [# ownw   : WriteSets,
                      clock  : real
                     #]
  
  sp: SemPrim =
    (# ownw := emptyset,
       clock:=0 #) 
  
  lem: LEMMA
         sp 
         =
         sp
           WITH [ownw := add((# data := 0, timestamp := 0 #),
                               emptyset)]
  %                            emptyset[DataItems])]
  END error
  
  --==_Exmh_5309712040--
  

How-To-Repeat: 

Fix: 
The bug was caused by a problem in the judgements mechanism related to
records.  On fixing this, it was noticed that the resulting TCC was
unprovable.  Further investigation showed a problem in the conversion
mechanism, which should apply the restrict conversion.  This has also been
fixed.

Note: it's still a good idea to provide the emptyset instance, as the type
of (# data := 0, timestamp := 0 #) is [# data: real, timestamp: real #].
restrict then is applied to the add(...) term.
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools