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

PVS Bug 531


Synopsis:        Strange COND-ENDCOND Paarse Errors
Severity:        serious
Priority:        medium
Responsible:     dave_sc (Dave Stringer-Calvert)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Wed Mar  7 12:20:03 2001
Originator:      "Mark A. Hillebrand"
Organization:    wjpserver.CS.Uni-SB.DE
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  Hi!
  
    I use PVS Version 2.3 (patch level 1.2.2.36).
  
    Using COND-ENDCOND gets me strange parsee errors. Consider the following
  
  wohnheimd: THEORY BEGIN
      t1: TYPE = { kann, sehr, viel };
      t2: TYPE = { fuenf, sechs, sieben };
  
      pred1(a:t1):bool;
      pred2(a:t1):bool; 
      pred3(a:t1):bool;
  
      rums(a:t1):t2 = COND
          (pred1(a) OR pred2(a)) -> fuenf,
          pred3(a) -> sechs,
          ELSE -> sieben
      ENDCOND
  END wohnheimd
  
  This breaks on M-x show-tccs with:
  
  Found ELSE when expecting
    opsym, (, (#, [|, (:, identifier, IF, TRUE, FALSE, [||], !STRING!,
  !NUMBER!, LAMBDA, FORALL, EXISTS, {, LET, CASES, COND, or TA
  BLE
  
  Changing the first COND line from
          (pred1(a) OR pred2(a)) -> fuenf,
  to  
          (pred1(a) OR pred2(a))::bool -> fuenf,
  removes this.
  
  Note: regular parsing (i.e. M-x parse) and type-checking (i.e. M-x
  tc) works in *both* cases.
   Mark Hillebrand
  ___
  mah@wjpserver.cs.uni-sb.de
  
  
  

How-To-Repeat: 

Fix: 

 [davesc, 7/21/01]
 Fixed.  See also bug # 580 reporting the same issue.

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