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

PVS Bug 744


Synopsis:        relative addressing not working right in PVS 3 libraries
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           open
Class:           sw-bug
Arrival-Date:    Wed Feb 19 14:10:00 2003
Originator:      Rick Butler
Organization:    larc
Release:         PVS 3.0
Environment: 
 System:          
 Architecture: 

Description: 
  Sam,
     I have encountered a SERIOUS problem with libraries
  in PVS 3.1.
  
  To see the problem, install the NASA libraries 
  
    http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/pvslib.html
  
  in the lib subdirectory of the PVS installation directory.
  A tar file of all of the libraries is available at a link labeled:
  
      PVS3.1 tar file with bins  
  
  In other words they are in there with "finite_sets" and "bitvectors".
  (Note. that's the way everybody here does it)
  
  Then put the following theory in a directory at a different level,
  e.g. your home directory.
  
    bug: THEORY
    BEGIN
    
     IMPORTING reals@sqrt
    % IMPORTING vectors@position2
    
     IMPORTING analysis@integral_def
    
    end bug
  
  Issue M-x tc and you will get:
  
     Library ../reals/ does not exist
  
  If you try this using PVS2 (assuming NASA libraries similarly
  installed) it works right.
  
  Note that the theory "integral_def" contains the following:
  
     reals: LIBRARY "../reals"
  
     IMPORTING reals@sigma
  
  
  I think this is what it cannot find because it is starting
  its search relative to the location of "bug" rather than
  relative to where the analysis library is.
  
  The same problem occurs if you uncomment out the
  IMPORTING vectors@position2 because it too uses the reals library.
  
  This is a serious problem because the NASA library is constructed
  with alot of cross-dependent IMPORTINGS.  This was fixed in PVS 2 
  and now has re-appeared in PVS 3.1
  
  Rick

How-To-Repeat: 

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