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

PVS Bug 706


Synopsis:        Attempt to store declaration in illegal theory
Severity:        serious
Priority:        medium
Responsible:     owre
State:           analyzed
Class:           sw-bug
Arrival-Date:    Wed Aug 14 10:40:00 2002
Originator:      Hendrik Tews
Organization:    tcs.inf.tu-dresden.de
Release:         PVS 2.4
Environment: 
 System:          
 Architecture: 

Description: 
  
  --DOmXUnlYcJ
  Content-Type: text/plain; charset=us-ascii
  Content-Description: message body text
  Content-Transfer-Encoding: 7bit
  
  Hi,
  
  I get the message in the subject line when I exit from PVS. 
  
  To reproduce the error:
  
  - untar the appended tar file
  - start pvs in directory hw
  - "yes" -- create a new context
  - M-x load-file typecheck.el
  - visit file virtual_memory.pvs
  - M-x tcp
  - fianally M-x save-context yields 
     "Attempt to store declaration in illegal theory"
  
  Bye,
  
  Hendrik
  
----spec removed----  

How-To-Repeat: 

Fix: 
Modified the recognizer-name slot of constructor-name-expr and the
constructor-name slot of recognizer-name-expr to make sure they aren't
copied or saved to the bin files.
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools