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

PVS Bug 1039


Synopsis:        TCC in generated _adt theory
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Mon May 19 11:35:00 -0700 2008
Originator:      Hendrik Tews
Release:         PVS 4.1
Organization:    cs.ru.nl
Environment: 
 System:          
 Architecture: 

Description: 
  Hi,
  
  in the PVS repository at
  http://www.cs.ru.nl/~tews/Robin/robin-hw-model-2008-05-15.tgz 
  there is a TCC in Pte_type_adt, which is generated for the data
  type Pte_type in paging-data.pvs. There are various problems with
  this TCC.
  
  1. The TCC seems to refer to line 67 in paging-data. There this
     TCC is suppressed, because it is subsumed by a similar TCC for
     line 43. But if it indeed refers to the declaration of
     Pte_4k_type, it should appear in theory Page_Directory_Types!
  
  2. There is no default proof associated with it, nevertheless it
     is proved during prove-importchain.
  
  3. It does not appear in the PVS Status buffer, but is counted
     during prove-importchain, leading to a discrepancy of the
     Grand Totals line in the PVS Status buffer and what is
     reported in the minibuffer. 
  
  
  Bye,
  
  Hendrik

How-To-Repeat: 

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