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

PVS Bug 1043


Synopsis:        missing TCC for COND
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Thu Oct 23 14:20:00 -0700 2008
Originator:      Kai Engelhardt
Release:         PVS 4.2
Organization:    cse.unsw.edu.au
Environment: 
 System:          
 Architecture: 

Description: 
  M-x tc fails to generate the (invalid in this example) TCC for the
  ELSE branch of COND stating that i should be of type bool, not nat.
  
  PVS Version 4.2 - Allegro CL Enterprise Edition 8.1 [Mac OS X (Intel)]  
  (Jul 22, 2008 4:19) - Allegro CL Enterprise Edition 8.1 [Mac OS X  
  (Intel)] (Jul 22, 2008 4:19)
  
  GNU Emacs 22.1.50.1 (i386-apple-darwin8.11.1, Carbon Version 1.6.0) of  
  2008-01-18 on seijiz.local
  
  Darwin MiniMeToo.local 9.5.0 Darwin Kernel Version 9.5.0: Wed Sep  3  
  11:29:43 PDT 2008; root:xnu-1228.7.58~1/RELEASE_I386 i386
  
  condbug: THEORY
  
     BEGIN
       i: VAR nat
       b: VAR bool
       h: VAR finseq[bool]
  
       foo(i,b,h): bool =
         h`length >= i &
         h`seq(i) = COND
                      i=0  -> true,
                      ELSE -> i
                    ENDCOND
     END condbug
  
  Cheers,
  Kai

How-To-Repeat: 

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