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

PVS Bug 1051


Synopsis:        Cursor does not point to the error location (VIII)
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Wed Apr 14 10:50:00 -0700 2010
Originator:      Hendrik Tews
Release:         PVS 4.2
Organization:    os.inf.tu-dresden.de
Environment: 
 System:          
 Architecture: 

Description: 
  
  --lkZKRnEBXk
  Content-Type: text/plain; charset=us-ascii
  Content-Description: message body text
  Content-Transfer-Encoding: 7bit
  
  Hi,
  
  the appended spec contains three errors. For each of them the
  cursor does not jump to the error location.
  
  1. First typecheck reports "Found 'MEASURE' when expecting
     'ENDIF'" with the cursor on line 39, where Measure is on line
     65 and the endif is missing before it.
  
  2. After uncommenting the endif on line 64 I get "Found 'MEASURE'
     when expecting 'END'" with the cursor still on line 39.
  
  3. After uncommenting the Recursive on line 25 I get
  
      first argument to critical_or_release_before_try_lock has the wrong type
  	 Found: Statement_adt.Statement
        Expected: list_adt[Statement].list
  
     with the cursor again on line 39, but the actual error is on
     line 41.
  
  Bye,
  
  Hendrik
  
  
  --lkZKRnEBXk
  Content-Type: application/octet-stream; name="position3.pvs"
  Content-Disposition: attachment;
  	filename="position3.pvs"
  Content-Transfer-Encoding: base64
  
  RXhwcmVzc2lvbiA6IERhdGF0eXBlCkJlZ2luCiAgdHJ5X2xvY2tfZnVuIDogdHJ5X2xvY2tfZnVu
  PwogIHRydWVfZXhwciA6IHRydWVfZXhwcj8KRW5kIEV4cHJlc3Npb24KClN0YXRlbWVudCA6IERh
  dGF0eXBlCkJlZ2luCiAgSW1wb3J0aW5nIEV4cHJlc3Npb24KCiAgbm90aGluZyA6IG5vdGhpbmc/
  CiAgY3JpdGljYWwgOiBjcml0aWNhbD8KICB1bmNyaXRpY2FsIDogdW5jcml0aWNhbD8KICByZWxl
  YXNlX3N0bSA6IHJlbGVhc2Vfc3RtPwogIHNlcXVlbmNlKHN0bV8xIDogU3RhdGVtZW50LCBzdG1f
  MiA6IFN0YXRlbWVudCkgOiBzZXF1ZW5jZT8KICBkb193aGlsZShzdG0gOiBTdGF0ZW1lbnQsIGNv
  bmRpdGlvbiA6IEV4cHJlc3Npb24pIDogZG9fd2hpbGU/CiAgaWZfc3RtKGNvbmRpdGlvbiA6IEV4
  cHJlc3Npb24sIHN0bSA6IFN0YXRlbWVudCkgOiBpZl9zdG0/CkVuZCBTdGF0ZW1lbnQKCkxvY2tQ
  cm9wZXJ0eSA6IFRoZW9yeQpCZWdpbgogIEltcG9ydGluZyBTdGF0ZW1lbnQKCiAgY3JpdGljYWxf
  b3JfcmVsZWFzZV9iZWZvcmVfdHJ5X2xvY2sodCA6IGxpc3RbU3RhdGVtZW50XSwgYm91bmQgOiBu
  YXQpIDogCiAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAg
  ICAgICAgIFJFQ1VSU0lWRQogICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAg
  ICAgICAgICAgICAgICAgICAgICAgICAgW2Jvb2wsIG5hdF0gPQogICAgSUYgYm91bmQgPSAwIFRo
  ZW4gKGZhbHNlLCAwKQogICAgRWxzZQogICAgICBDYXNlcyB0IE9GCiAgICAgICAgbnVsbCA6IChm
  YWxzZSwgYm91bmQpLAogICAgICAgIGNvbnMocywgcmVzdCkgOiAKICAgICAgICAgIENhc2VzIHMg
  T0YKICAgICAgICAgICAgbm90aGluZyA6IGNyaXRpY2FsX29yX3JlbGVhc2VfYmVmb3JlX3RyeV9s
  b2NrKHJlc3QsIGJvdW5kIC0gMSksCiAgICAgICAgICAgIGNyaXRpY2FsIDogKHRydWUsIGJvdW5k
  KSwKICAgICAgICAgICAgdW5jcml0aWNhbCA6IGNyaXRpY2FsX29yX3JlbGVhc2VfYmVmb3JlX3Ry
  eV9sb2NrKHJlc3QsIGJvdW5kIC0gMSksCiAgICAgICAgICAgIHJlbGVhc2Vfc3RtIDogKHRydWUs
  IGJvdW5kKSwKICAgICAgICAgICAgc2VxdWVuY2UoczEsIHMyKSA6IAogICAgICAgICAgICAgIGNy
  aXRpY2FsX29yX3JlbGVhc2VfYmVmb3JlX3RyeV9sb2NrKGNvbnMoczEsIGNvbnMoczIsIHJlc3Qp
  KSwKICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICBib3Vu
  ZCAtIDEpLAogICAgICAgICAgICBkb193aGlsZShzMSwgYykgOiAKICAgICAgICAgICAgICBsZXQg
  cmVzX2JvdW5kID0gY3JpdGljYWxfb3JfcmVsZWFzZV9iZWZvcmVfdHJ5X2xvY2soczEsIGJvdW5k
  KQogICAgICAgICAgICAgICVsZXQgcmVzX2JvdW5kID0gY3JpdGljYWxfb3JfcmVsZWFzZV9iZWZv
  cmVfdHJ5X2xvY2soKDpzMTopLCBib3VuZCkKICAgICAgICAgICAgICBJTgogICAgICAgICAgICAg
  ICAgSUYgUHJval8xKHJlc19ib3VuZCkgVGhlbiByZXNfYm91bmQKICAgICAgICAgICAgICAgIEVs
  c2lmIFByb2pfMihyZXNfYm91bmQpID0gMCBUaGVuIHJlc19ib3VuZAogICAgICAgICAgICAgICAg
  RWxzaWYgYyA9IHRyeV9sb2NrX2Z1biBUaGVuIChmYWxzZSwgMCkKICAgICAgICAgICAgICAgIEVs
  c2UgY3JpdGljYWxfb3JfcmVsZWFzZV9iZWZvcmVfdHJ5X2xvY2socmVzdCwgCiAgICAgICAgICAg
  ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIFByb2pfMihyZXNf
  Ym91bmQpKQogICAgICAgICAgICAgICAgRW5kaWYsCiAgICAgICAgICAgIGlmX3N0bShjLCBzMSkg
  OiAKICAgICAgICAgICAgICBJRiBjID0gdHJ5X2xvY2tfZnVuCiAgICAgICAgICAgICAgVGhlbiBj
  cml0aWNhbF9vcl9yZWxlYXNlX2JlZm9yZV90cnlfbG9jayhjb25zKHMxLCByZXN0KSwKICAgICAg
  ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIGJvdW5kIC0g
  MSkKICAgICAgICAgICAgICBFbHNlCiAgICAgICAgICAgICAgICBMZXQgcmVzX2JvdW5kID0KICAg
  ICAgICAgICAgICAgICAgICAgICAgICBjcml0aWNhbF9vcl9yZWxlYXNlX2JlZm9yZV90cnlfbG9j
  aygoOiBzMSA6KSwgYm91bmQpCiAgICAgICAgICAgICAgICBJTgogICAgICAgICAgICAgICAgICBJ
  RiBQcm9qXzEocmVzX2JvdW5kKSB0aGVuIHJlc19ib3VuZAogICAgICAgICAgICAgICAgICBFbHNl
  IGNyaXRpY2FsX29yX3JlbGVhc2VfYmVmb3JlX3RyeV9sb2NrKHJlc3QsIGJvdW5kKQogICAgICAg
  ICAgICAgICAgICBFbmRpZgogICAgICAgICAgICAgIEVuZGlmCiAgICAgICAgICBFbmRDYXNlcwog
  ICAgICBFbmRDYXNlcwogICAgRW5kaWYKICBNZWFzdXJlIGJvdW5kCkVuZCBMb2NrUHJvcGVydHkK
  --lkZKRnEBXk--

How-To-Repeat: 

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