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

PVS Bug 1064


Synopsis:        type check conditions bug?
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Wed Jul 21 16:35:00 -0700 2010
Originator:      Mu Sun
Release:         PVS 4.2
Organization:    illinois.edu
Environment: 
 System:          
 Architecture: 

Description: 
  Problem Description:
  =================
  Specification is type checked, but the type check conditions cannot be
  printed with "M-x tcc"
  
  
  System Info:
  ==========
  PVS Version 4.2 - Allegro CL Enterprise Edition 8.1 [Linux (x86)] (Jul
  22, 2008 3:35) - Allegro CL Enterprise Edition 8.1 [Linux (x86)] (Jul
  22, 2008 3:35)
  
  GNU Emacs 23.1.1 (x86_64-pc-linux-gnu, X toolkit, Xaw3d scroll bars)
  of 2010-03-29 on yellow, modified by Debian
  
  Linux musun-desktop 2.6.32-23-generic #37-Ubuntu SMP Fri Jun 11
  08:03:28 UTC 2010 x86_64 GNU/Linux
  
  
  Specification:
  ===========
  play2  % [ parameters ]
  		: THEORY
  
    BEGIN
  
    % ASSUMING
     % assuming declarations
    % ENDASSUMING
  
    T1 : TYPE = {a, b, c}
    T2 : TYPE = {1, 2, 3}
  
    T : TYPE = [T1 + T2]
  
    t1?(t:T) : bool = IN?_1(t)
    t1??(t:T) : bool = IN?_1(t)
    t1(t:(t1?::pred[T])) : T1 =
    	OUT_1(t)
  
    f(t:(t1??)) : T1 = t1(t)
  
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%
    % Parse error in 'M-x tcc' %
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%
  
    END play2

How-To-Repeat: 

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