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

PVS Bug 754


Synopsis:        Symbol's function definition is void: set-prelude-files-and-regions
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Mon Mar 24 07:30:01 2003
Originator:      Hendrik Tews
Organization:    tcs.inf.tu-dresden.de
Release:         PVS 3.1
Environment: 
 System:          
 Architecture: 

Description: 
  Hi,
  
  consider the following theory
  
      A : Theory
      Begin
        IMPORTING bitvectors@top
  
      End A
  
  if you invoke (after typechecking) find-declaration with bvec0
  and type s in the Browse buffer PVS answers with
  
     pvs-browse-select: Symbol's function definition is void: set-prelude-files
 -and-regions
  
  Bye
  
  Hendrik

How-To-Repeat: 

Fix: 
Appears to have been fixed earlier.
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools