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

PVS Bug 390


Synopsis:        Bug in the COMMENT command?
Severity:        serious
Priority:        medium
Responsible:     dave_sc (Dave Stringer-Calvert)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Wed Nov 24 17:40:01 1999
Originator:      srivas
Organization:    csl.sri.com
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  
  I notice that (sometimes) PVS puts a a string, i.e., "...", rather
  than commented text when it repeats the message argument of the
  COMMENT command iniside the proof script it stores.  This creates
  problem when rerunnning andn installiing old proofs.
  
  - Srivas

How-To-Repeat: 
(Owre 2001-08-06)
I couldn't actually repeat this one.  I suspect that it is related to
*print-length* being set to a low number, which can happen in certain
kinds of breaks.  If a proof is started while in such a break, this
behavior might be seen.
Fix: 
(Owre 2001-08-06)
Modified comment-step to set the *print-length* and *print-level* to nil
prior to invoking semi-colonize.
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools