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

PVS Bug 1068


Synopsis:        Typechecker Bug
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Wed Sep 29 15:05:01 -0700 2010
Originator:      "Munoz, Cesar Augusto (LARC-D320)"
Release:         PVS 4.2
Organization:    nasa.gov
Environment: 
 System:          
 Architecture: 

Description: 
  Sam,
  
  I wonder if you can take a look at the following type checking error, which
  is driving me crazy.
  
  I'm sorry but I was not able to isolate the problem, so to reproduce it you
  will need the latest NASA libraries and the theories in the following tgz
  file:
  
  ... Removed ...
  
  Go to the file top.pvs in ACCoRD and typecheck it for the first time, e.g.,
  no .pvscontext file and no pvsbin directory. You get the non-informative
  error:
  
  Error: No methods applicable for generic function
  
  If you ignore the error, then *usually* you can typecheck the file the
  second time you try, but sometimes you get some erratic behavior such as
  nothing seems to happen and you need to reset pvs.
  
  So far, this is what I know. If you comment the last 3 IMPORTINGs in
  top.pvs, then there is no problem. Furthermore, if you go directly to any of
  these files and typecheck from there, there is no problem either.
  
  I can reproduce the error in mac and linux with PVS Version 4.2, all patches
  included (and no patches included as well).
  
  Cesar
  
  
  On 9/29/10 4:33 AM, "Sam Owre" <owre@csl.sri.com> wrote:
  
  > Butler, Ricky W. (LARC-D320) <r.w.butler@nasa.gov> wrote:
  > 
  >> Sam,
  >>     Here is another PVS bug that is a high priority for us to have fixed.
  >> It may be centered around a clash between our fseqs theory (structures
  >> library) and the finite sequences in the prelude.  I wonder if it would be
  >> advantageous to restructure the PVS prelude into layers, e.g. layer 0 = ba
 re
  >> essentials, layer 1 = basic functions and theories, layer 2 adds the rest
  >> with the ability of the users to only have layer 0 or layer 1 or layer 2 v
 ia
  >> some start-up option.
  >> 
  
  
  -- 
  Cesar A. Munoz                             NASA Langley Research Center
  Cesar.A.Munoz@nasa.gov                     Bldg. 1220  Room 115 MS. 130
  http://shemesh.larc.nasa.gov/people/cam    Hampton, VA 23681-2199, USA
  Office: +1 (757) 864 1446                  Fax: +1 (757) 864 4234
  

How-To-Repeat: 

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