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

PVS Bug 792


Synopsis:        No methods applicable for generic function with bin files
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Wed Jul 23 09:45:01 2003
Originator:      Hendrik Tews
Organization:    tcs.inf.tu-dresden.de
Release:         PVS 3.1
Environment: 
 System:          
 Architecture: 

Description: 
  
  --vjqEqJn5hw
  Content-Type: text/plain; charset=us-ascii
  Content-Description: message body text
  Content-Transfer-Encoding: 7bit
  
  Hi,
  
  pvs crashes with the "no methods applicable" error if it loads a
  bin file for a theory that refers to a library owned by the same
  user.
  
  Example:
  
  - untar and change into lib-user/lib
  - produce A.bin and context by typechecking A
  - change into lib-user/B
  - Adjust the library declaration in B.pvs, keep an absolut path
  - produce B.bin and context in lib-user/B
  - start pvs again in lib-user/B and typecheck B
  
  Known workarounds:
  - use a relative path in the library declaration
  - write protect the library and use a different owner for it
  
  Bye,
  
  Hendrik
  
  
  --vjqEqJn5hw
  Content-Type: application/octet-stream
  Content-Disposition: attachment;
  	filename="lib-user.tar.gz"
  Content-Transfer-Encoding: base64
  
  H4sIAJ2FHj8AA+3W32qDMBQGcK99itD7LYkmCoPCFMYo7I+MvoAy2wnWDaOOvv1O2q7rKGvpqO5i
  3+8mQQ4S8ulJyiK7aE1ec6c/QigRak0jzXSwGkXgrcc1R4Qh1QgZ2DopVaAcpntc01ZrmrRmzGny
  d3OojspmsyEWNKzyM3+a9PUNnJC/p3VI+Xuej/wH8S3/6PKtO7gJvyMkxa3Uz/kr/fX/K0n1vvR9
  h4nzL2XfP88/Ylds+pK/1ks3zudF5TKW0qOiatiY+e5N9cwi968XCb3Z/v9xfzeAk/p/aPs/XQMk
  +v8QdvKP++n+x/u/tJlv8hdhYM9/HQj0/yHE+/2fPgl6eFdkdVov6RQYcdNWvLFFRc7tPvGkLrq0
  4UlneNbODd+9RYzoFZP75PFpOnm4tS+7jtzNqVLmi0VKszHTq5MlxskCAAAAAAAAAAAAAAAAcE4f
  ii5ggwAoAAA=
  --vjqEqJn5hw--

How-To-Repeat: 

Fix: 
Fixed in the general fix for bin files.
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools