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

PVS Bug 474


Synopsis:        ITHEORY assertion
Severity:        serious
Priority:        medium
Responsible:     dave_sc (Dave Stringer-Calvert)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Mon Jul 17 10:20:07 2000
Originator:      Christoph Berg
Organization:    wurzelausix.cs.uni-sb.de
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  Hello,
  
  we have a problem while trying to import a file from a different context.
  Typechecking a theory that only contains a "import lib@theory" leads to
  the message "Error: the assertion ITHEORY failed." in the *Error Output*
  buffer. The imported file typechecks ok for itself.
  
  The error disappears when the file is moved to the first file's context.
  
  We think that this is caused by using relative paths in a directory tree
  of contexts, e.g. 'lib: library "../lib" ' would appear as 'lib: library
  "../../lib" ' or 'lib: library "../other_context/lib" ' depending on the
  relative position in the file system.
  
  Seemingly, the problem disappears if a flat directory structure is used,
  i.e.  all references are of the form 'lib: library "../lib" '.
  
  We use PVS Version 2.3 (patch level 1.2.2.36) on FreeBSD 4.0 (using the
  Linux emulation).
  
  I see that this has previously been reported as bug #445, I hope my
  comments help to solve the problem. In case of interest, the files causing
  the error message.
  
  Christoph Berg
  -- 
  Lehrstuhl für Rechnerarchitektur
  Universität des Saarlandes, Saarbrücken, Germany
  http://www-wjp.cs.uni-sb.de/~cb/ , +49/681/302-4490, -4290 (Fax)
  
  

How-To-Repeat: 

Fix: 

 [davesc]
 Fixed in 2.3.1

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