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

PVS Bug 629


Synopsis:        how to repeat the PROGRAM ERROR
Severity:        serious
Priority:        medium
Responsible:     owre
State:           analyzed
Class:           sw-bug
Arrival-Date:    Fri Dec  7 18:45:23 2001
Originator:      Marcelo Glusman
Organization:    cs.technion.ac.il
Release:         PVS 2.4
Environment: 
 System:          
 Architecture: 

Description: 
  Hi Sam,
  I finished porting all my proofs to PVS2.4, working around the problems.
  They take 387 seconds.
  With PVS2.3, they take 460 seconds.
  
  If you want to debug the problem with GRIND on updated records, download
  the dump from http://www.cs.technion.ac.il/~marce/conv_comp/index.html
  The file http://www.cs.technion.ac.il/~marce/conv_comp/top.dump_2.3.gz
  has the old proofs.
  Enter theory: pipeline_sort
  Step over the proof of: input_layers_ordered
  Stop before line number: 33, which looks like:
    (("1" (SPLIT) (("1" (HIDE -3) (GRIND)) ("2" (SKOSIMP*) (GRIND))))
                                   ^^^^^                    ^^^^^
  If you execute any of those two (GRIND)s you get the message:
  Error: No methods applicable for generic function
         #<STANDARD-GENERIC-FUNCTION ROW-EXPR> with args...
  ...
    [condition type: PROGRAM-ERROR]
  ...
  SPC-scroll, I-ignore, etc etc.
  
  Hope this helps fix a bug,
  Marcelo.
  

How-To-Repeat: 

Fix: 
Modified substit* :around (table-expr) to check that nexpr is a table-expr
before treating it as one.
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools