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

PVS Bug 942


Synopsis:        PVS release candidate
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           open
Class:           sw-bug
Arrival-Date:    Tue Jan 24 11:55:00 2006
Originator:      Hendrik Tews
Organization:    tcs.inf.tu-dresden.de
Release:         PVS 3.3 release candidate
Environment: 
 System:          
 Architecture: 

Description: 
  
  --Boundary_(ID_jwrrqRwVtxNOGsaDzm9k4Q)
  Content-type: text/plain; charset=us-ascii
  Content-transfer-encoding: 7BIT
  Content-description: message body text
  
  Hi Sam,
  
     I have a new release candidate for you to try; it's in
     ftp://ftp.csl.sri.com/pub/users/owre/pvs3.3-release-candidate/
     
  Thanks for the work you put into it. I found the following
  problems:
  
  1. with x-step-proof there is lots of clutter in *pvs*, like
  
  sending wish cmd:
   setup-proof types_ok_p_skip PVariables2 /tmp/tews/Semantics/ 1 1
  
  2. *features* still contains pvs3.2
  
  3. Bug #889: there is no error message any more. However, instead
     of installing the current proof is deleted.
  
  4. PVS 3.3 gives now the parser error 
  
  Theory Z is declared in theory-interpretation16.pvs and theory-interpretation
 17.pvs
  
     instead of asking whether to override. If I want to continue
     parsing, is there an alternative to restarting Pvs?
  
  5. in Bug 930: ppti breaks in the cases a,b,d
  
  6. in bug 758: Exchange YImp with the following to make it
     correct:
  
     YImp : Theory
     Begin
       ZImp : Theory = Z{{z := 5}}
       IMPORTING Y{{My_Z := ZImp, y:=5}}
     End YImp
  
     then ppti on Y gives
  
     Y: THEORY
      BEGIN
  
       IMPORTING ZImp
  
       My_Z: THEORY = YImp
                      ^^^^
      END Y
  
  7. The appended (incorrect) file theory-interpations15 gives an
  
       error in process filter: Window height 1 too small (after splitting)
  
     maybe, because the error message file in /tmp is empty.
  
  
  8. Bug 758 can IMHO be closed now.
  
  9. Bug 785. The appended file datatype-updates.pvs gives 
  
       Error: attempt to take the length of a non-sequence: (cons?[int])
  
     it works fine in 3.2 and also 3.3 beta. (This means #785 can
     be closed for 3.2)
  
  10. (finally reached the biblical number) Can you have a look at
      Bug 921? It is a showstopper for unused-by-* and it seems
      pretty trivial to fix.
  
  Bye,
  
  Hendrik
  
  
  --Boundary_(ID_jwrrqRwVtxNOGsaDzm9k4Q)
  Content-type: application/octet-stream; NAME=theory-interpretation15.pvs
  Content-transfer-encoding: base64
  Content-disposition: attachment; filename=theory-interpretation15.pvs
  
  JSBvayBhcyBpdCBpcyB3aXRoIDMuMyBiZXRhCiUgdW5jb21tZW50IEltcG9ydGluZyBZMVtaMV06
  IEVycm9yOiB0aGUgYXNzZXJ0aW9uIGFtYXAgZmFpbGVkCiUgZml4ZWQgaW4gMy4zIGdhbW1hCiUg
  Y29tbWVudCBpbXBvcnRpbmcgX2FuZF8gWjIgZGVjbCBnaXZlcwolICAgIGVycm9yIGluIHByb2Nl
  c3MgZmlsdGVyOiBXaW5kb3cgaGVpZ2h0IDEgdG9vIHNtYWxsIChhZnRlciBzcGxpdHRpbmcpCiUg
  KG1heWJlIGJlY2F1c2UgZXJyb3IgbWVzc2FnZSBpbiAvdG1wIGlzIGVtcHR5CgpaIDogVGhlb3J5
  CkJlZ2luCiAgeiA6IGludAogIHUgOiBuYXQKICB6YSA6IEF4aW9tIHogPiB1CkVuZCBaCgpZW015
  X1ogOiBUaGVvcnkgWl0gOiBUaGVvcnkKQmVnaW4KICB5IDogaW50CgogIHp5IDogQXhpb20geiA9
  IHkKRW5kIFkKCloxIDogVGhlb3J5CkJlZ2luCiAgejEgOiBpbnQgPSA0CiAgdTEgOiBuYXQKICB6
  MWEgOiBBeGlvbSB1MSA8IDIKRW5kIFoxCgpaMUltcCA6IFRoZW9yeQpCZWdpbgogIEltcG9ydGlu
  ZyBaMQogIElNUE9SVElORyBae3t6Oj16MSwgdTo9dTF9fQpFbmQgWjFJbXAKCgpZMVtNeV9aIDog
  VGhlb3J5IFoxXSA6IFRoZW9yeQpCZWdpbgogIHkxIDogaW50ID0gNAogIHp5MSA6IExlbW1hIE15
  X1ouejEgPSB5MQpFbmQgWTEKCgpZMUltcCA6IFRoZW9yeQpCZWdpbgolICBJbXBvcnRpbmcgWTFb
  WjFdCiUgIFoyIDogVGhlb3J5ID0gWnt7eiA6PSA0fX0KICBJTVBPUlRJTkcgWVtaMl17e3k6PTR9
  fQpFbmQgWTFJbXAKCgo=
  
  --Boundary_(ID_jwrrqRwVtxNOGsaDzm9k4Q)
  Content-type: application/octet-stream; NAME=datatype-updates.pvs
  Content-transfer-encoding: base64
  Content-disposition: attachment; filename=datatype-updates.pvs
  
  JSBidWcgNzg1CiUgc2VlbXMgdG8gYmUgZml4ZWQgaW4gMy4yCgpYIDogVGhlb3J5CkJlZ2luCiAg
  bCA6IGxpc3RbbmF0XSA9ICg6IDAsIDEsIDIgOik7CgogIHIgOiBsaXN0W25hdF0gPSBsICBXSVRI
  IFtgY2FyIDo9IDFdCgogIG5vdF9udWxsIDogTGVtbWEgY29ucz8ocikKCiAgeCA6IExlbW1hIGxl
  bmd0aChyKSA9IDQgIAplbmQgWAo=
  
  --Boundary_(ID_jwrrqRwVtxNOGsaDzm9k4Q)--

How-To-Repeat: 

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