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

PVS Bug 871


Synopsis:        PVS not exited
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           open
Class:           sw-bug
Arrival-Date:    Wed Nov 24 15:40:00 2004
Originator:      Hendrik Tews
Organization:    tcs.inf.tu-dresden.de
Release:         PVS 3.2
Environment: 
 System:          
 Architecture: 

Description: 
  Hi Sam,
  
  thanks for your quick patch. It solves the problem that I
  reported.
  
  However, with the patch I can reproduce a (non-critical) problem
  that I noticed before:
  
  - load and typecheck programms-4 (presumably in a fresh context)
  - try to exit immediately afterwards
  
  Doing this I get an emacs error and the *Message* buffer contains
  
  ....
  PVS is garbage collecting...
  Finished garbage collecting
  TestPrograms4 typechecked in 24.27s: 123 TCCs, 0 proved, 67 subsumed, 56 unpr
 oved; 80 msgs
  (No files need saving)
  Created directory /tmp/tews/Sem/pvsbin
  byte-code: PVS not exited

  Bye,
  
  Hendrik

How-To-Repeat: 

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