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

PVS Bug 388


Synopsis:        bug after add-declaration
Severity:        serious
Priority:        medium
Responsible:     dave_sc (Dave Stringer-Calvert)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Wed Nov 24 03:40:21 1999
Originator:      Marcelo Glusman
Organization:    csl.sri.com
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  Hi,
  I wanted to test the add-declaration in the middle of a proof
  (again).
  
  First, I saw that the bug that used to happen when adding a declaration
  at the beginning of the current theory (before any other declaration)
  is still there.
  So I put a dummy declaration at the beginning.
  
  This is the theory before the added decl:
  --------------
  try : THEORY
  BEGIN
    dummy: CLAIM FORALL(n:nat): n>=0
  
    % added decl will come here
  
    garbage: CLAIM FORALL(n:nat): n>2
  END try
  
  I started to prove "garbage" with a (skosimp*).
  
  I then placed the pointer at the % above, and issued M-x add-declaration.
  
  In the new buffer, I typed:
    moregarbage: CLAIM FORALL(n:nat): n>3
  
  C-c C-c worked fine. I then used (USE "moregarbage") (ASSERT)
  and the proof was done. But then look what happened:
  
  Context was modified in mid-proof.
  Would you like to rerun the proof? (Yes or No) yes
  Error: `NIL' is not of the expected type `HASH-TABLE'
    [condition type: TYPE-ERROR]
  
  Restart actions (select using :continue):
   0: Return to Top Level (an "abort" restart)
  [1] PVS(35): 
  
  
  

How-To-Repeat: 

Rule? (assert)
Simplifying, rewriting, and recording with decision procedures,
Q.E.D.

Context was modified in mid-proof.
Would you like to rerun the proof? (Yes or No) yes
Error: `NIL' is not of the expected type `HASH-TABLE'
  [condition type: TYPE-ERROR]

Restart actions (select using :continue):
 0: Return to Top Level (an "abort" restart)
[1] PVS(20): :bt
Evaluation stack:

HASH-TABLE-SIZE <-
  COPY-SUBST-MOD-PARAMS-CACHE <- (METHOD PROVE-DECL (FORMULA-DECL)) <-
  (:INTERNAL (:EFFECTIVE-METHOD 1 T ...) 0) <- SAVE-PROOF-INFO <-
  (METHOD PROVE-DECL (FORMULA-DECL)) <-
  (:INTERNAL (:EFFECTIVE-METHOD 1 T ...) 0) <-
  (METHOD PROVE (FORMULA-DECL)) <-
  (:INTERNAL (:EFFECTIVE-METHOD 1 T ...) 0) <- PROVE-FILE-AT <- EVAL <-
  TPL:TOP-LEVEL-READ-EVAL-PRINT-LOOP <- TPL:START-INTERACTIVE-TOP-LEVEL


Fix: 
[owre 2001-07-24]
Fixed the way the hash-table was being copied - it was creating the new
hash-table, but not actually returning it.  The underlying code is
fault-tolerant enough that this went undetected until analysing this bug.
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools