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

PVS Bug 414


Synopsis:        adding declarations
Severity:        serious
Priority:        medium
Responsible:     owre
State:           analyzed
Class:           sw-bug
Arrival-Date:    Wed Jan  5 10:40:08 2000
Originator:      Marcelo Glusman
Organization:    cs.technion.ac.il
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  Hi,
  
  The add-declarations feature has a couple of problems, even with the
  Christmas patch:
  
  1 - As I previously reported, there's an
      "Error: no methods applicable for generic function" bug
      when trying to add a declaration at the beginning of the
      theory.
  
  2 - After adding a declaration in the middle of a proof, finishing the
      proof and rerunning it as offered by the system, PVS seems to believe
      that the checker is still running. If I try to exit, it says:
      "Must exit the checker first", even when the proof is over.
  
  regards,
  
  Marcelo

How-To-Repeat: 

Fix: 
1 - Modified typecheck-new-decls to handle the situation where the added
    declaration is the first one.
2 - Modified save-proof-info to let *in-checker* to nil before invoking
    prove-decl recursively.
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools