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

PVS Bug 733


Synopsis:        Illegal instruction when dumping
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           open
Class:           sw-bug
Arrival-Date:    Wed Jan 29 09:50:00 2003
Originator:      Jerry James
Organization:    eecs.ku.edu
Release:         PVS 3.0
Environment: 
 System:          
 Architecture: 

Description: 
  I am releasing the PVS 3.0 version of my set theory library today.
  All but one of the dump files were created with no problem.  Attempting
  to create the last one results in the message:
  
  Error: Received signal number 4 (Illegal instruction)
  
  I can reliably reproduce this.  The full library is available from
  <URL:http://www.ittc.ku.edu/consistency/pvs/>.  The "infinite_sets"
  library is the one exhibiting the problem.  This is on an x86 RedHat
  Linux 7.3 box.
  
  This also exposes an error-handling bug in get-pvs-file-dependencies
  (pvs-utils.el).  When the dump error happens, pvs-send-and-wait returns
  the symbol 'Error: (an exploded version of the error string?) instead of
  the expected list, which causes the remove-if 3 lines further down to
  complain:
  
  (wrong-type-argument listp Error:)
  
  Regards,
  -- 
  Jerry James
  Assistant Professor
  EECS Department
  University of Kansas

How-To-Repeat: 

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