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

PVS Bug 494


Synopsis:        PVS 2.3 tc crash upon switching two definitions
Severity:        serious
Priority:        medium
Responsible:     dave_sc (Dave Stringer-Calvert)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Thu Nov  2 18:40:07 2000
Originator:      Paul Y Gloess
Organization:    labri.u-bordeaux.fr
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  This is a multi-part message in MIME format.
  --------------3E87B8B4B825B5B6335CDD49
  Content-Type: text/plain; charset=us-ascii
  Content-Transfer-Encoding: 7bit
  
  Dear PVS hackers:
  
  Rodolphe Pueyo found a bug with PVS 2.3: PVS crashes when two
  definitions are switched. Note that the same error arises whether the
  patches are loaded or not.
  
  The attached self explanatory dump was generated with the patches
  loaded.
  
  Best regards,
  
  --
  Paul Y Gloess
            LaBRI:   http://dept-info.labri.u-bordeaux.fr/~gloess
     E.N.S.E.R.B.:   http://www.enserb.u-bordeaux.fr/~gloess
  
  
  
  --------------3E87B8B4B825B5B6335CDD49
  Content-Type: text/plain; charset=us-ascii;
   name="bug.fun_order_crash.2_november_2000.dump.dump"
  Content-Transfer-Encoding: 7bit
  Content-Disposition: inline;
   filename="bug.fun_order_crash.2_november_2000.dump.dump"
  
  %Patch files loaded: patch2 version 1.2.2.36
  
  $$$dump.pvs
  %%%
  %%% Paul Y Gloess <Paul.Gloess@LaBRI.U-Bordeaux.Fr>
  %%%   http://dept-info.labri.u-bordeaux.fr/~gloess/
  %%%   http://www.enserb.fr/~gloess/
  %%%
  %%% Bug report, 2 november 2000, with PVS 2.3 (and above patches):
  %%%
  %%% Bug found by Rodolphe Pueyo.
  %%%
  %%% PVS crashes upon type checking when "fun2" is defined right after "fun1",
  %%%  unlike in the present "dump" theory: see error message in comment below.
  %%%
  dump [str: TYPE]: THEORY
  
    BEGIN
  
      IMPORTING data_type[str]
  
      IMPORTING list_to_set[element[str]]
  
      %%
      %% When "fun2" definition is placed right after "fun1" definition,
      %%  the following error arises upon type checking the theory:
      %%  Error: the assertion (FULLY-INSTANTIATED? DOMTYPES) failed.
      %%
      fun2(l: list[element[str]]): setof[element[str]]
        = set(l) ;
  
      fun1(l: list[element[str]]): RECURSIVE list[str]
        = CASES l OF
            null: null,
            cons(e, lr): fun1(lr)
          ENDCASES
        MEASURE identity BY << ;
  
    END dump
  
  $$$dump.prf
  (|dump|
   (|fun1_TCC1| "" (REWRITE "lambda_well_founded")
    (("" (REWRITE "list_well_founded[element[str]]") NIL NIL)) NIL)
   (|fun1_TCC2| "" (TERMINATION-TCC) NIL NIL)
   (|fun1_TCC3| "" (CASES-TCC) NIL NIL))
  
  
  $$$list_to_set.pvs
  list_to_set[T: TYPE]: THEORY
  
    BEGIN
  
      set(l: list[T]): setof[T]
        = {t: T | member(t, l)} ;
  
    END list_to_set
  
  $$$data_type.pvs
  data_type[str: TYPE]: THEORY
  
    BEGIN
  
      data_type: DATATYPE
        WITH SUBTYPES element
  
      BEGIN
  
        Element(s: str): Element?: element
  
      END data_type
  
    END data_type
  
  --------------3E87B8B4B825B5B6335CDD49--

How-To-Repeat: 

Fix: 

 [davesc]
 Fixed in 2.3.1

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