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

PVS Bug 901


Synopsis:        Directory name with & causes PVS to crash
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Thu Apr  7 10:05:00 2005
Originator:      Hanne Gottliebsen
Organization:    dcs.qmul.ac.uk
Release:         PVS 3.2
Environment: 
 System:          
 Architecture: 

Description: 
  With a directory name which includes & (eg. Spec&Ver) certain errors in 
  a specification will cause PVS to crash.
  
  For example: (note the {} for D)
  
  test: THEORY
     BEGIN
  
     N : NONEMPTY_TYPE
  
     S : NONEMPTY_TYPE
  
     D : TYPE = {N -> S}
  
  END test
  
  Upon typechecking, I get:
  
  error in process filter: apply: Wrong number of arguments:
  
  - Followed by a lot more.
  
  After this PVS still shows that it is typechecking and exiting does not 
  work (PVS not exited).
  
  
  Ofcourse, the easy solution (for me) is to not use & in directory names 
  (I do not, and next year I will make sure that my student do not either).
  
  
  Thanks,
  Hanne
  -- 
  ---------------------------------------------------------
  Dr. Hanne Gottliebsen    Department of Computer Science
  hago@dcs.qmul.ac.uk      Queen Mary, University of London
  Ph: +44 (0) 207 882 5259
     - I want a single-skin cotton tent like Mr Weasley's
  ---------------------------------------------------------

How-To-Repeat: 

Fix: 
The ampersand is used as a delimiter in messages sent to Emacs from PVS.
Fixed this so that embedded &'s are escaped.
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools