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

PVS Bug 1024


Synopsis:        Unfinished TCCs in _adt file
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           open
Class:           sw-bug
Arrival-Date:    Sun Jan 20 18:15:00 2008
Originator:      "Alejandro Tamalet"
Organization:    gmail.com
Release:         PVS 4.1
Environment: 
 System:          
 Architecture: 

Description: 
  ------=_Part_8877_29820388.1200871678045
  Content-Type: text/plain; charset=ISO-8859-1
  Content-Transfer-Encoding: 7bit
  Content-Disposition: inline
  
  Hi,
  
  When running the proof of our specification, on the PVS Status buffer we
  get:
  
  Grand Totals: 502 proofs, 502 attempted, 502 succeeded (2053.33 s)
  
  However, the PVS Log buffer says:
  
  MSG(Jan 21 00:01:00): CorrectnessAnnProgram: 520 proofs attempted, 512
  proved in 2069.89 real, 2069.89 cpu seconds
  
  I found some messages like:
  
  MSG(Jan 20 23:25:28): Body_Plus_eta_TCC2 unproved in 1.05 real, 1.05 cpu
  seconds
  MSG(Jan 20 23:25:28): Rerunning proof of Body_Plus_eta_TCC3
  MSG(Jan 20 23:25:29): Body_Plus_eta_TCC3 unproved in 1.01 real, 1.01 cpu
  seconds
  MSG(Jan 20 23:25:29): Rerunning proof of Body_Conj_eta_TCC1
  MSG(Jan 20 23:25:29): Body_Conj_eta_TCC1 proved in 0.79 real, 0.79 cpu
  seconds
  MSG(Jan 20 23:25:30): Rerunning proof of Body_Conj_eta_TCC2
  MSG(Jan 20 23:25:37): Body_Conj_eta_TCC2 unproved in 1.18 real, 1.18 cpu
  seconds
  MSG(Jan 20 23:25:37): Rerunning proof of Body_Conj_eta_TCC3
  MSG(Jan 20 23:25:38): Body_Conj_eta_TCC3 unproved in 1.15 real, 1.15 cpu
  seconds
  MSG(Jan 20 23:25:38): Rerunning proof of Body_Eq_eta_TCC1
  MSG(Jan 20 23:25:39): Body_Eq_eta_TCC1 proved in 0.80 real, 0.80 cpu seconds
  MSG(Jan 20 23:25:39): Rerunning proof of Body_Eq_eta_TCC2
  MSG(Jan 20 23:25:40): Body_Eq_eta_TCC2 unproved in 1.18 real, 1.18 cpu
  seconds
  MSG(Jan 20 23:25:40): Rerunning proof of Body_Eq_eta_TCC3
  MSG(Jan 20 23:25:41): Body_Eq_eta_TCC3 unproved in 1.09 real, 1.09 cpu
  seconds
  MSG(Jan 20 23:25:42): Rerunning proof of Body_StmtExpr_eta_TCC1
  MSG(Jan 20 23:25:42): Body_StmtExpr_eta_TCC1 proved in 0.77 real, 0.77 cpu
  seconds
  MSG(Jan 20 23:25:42): Rerunning proof of Body_StmtExpr_eta_TCC2
  MSG(Jan 20 23:25:43): Body_StmtExpr_eta_TCC2 unproved in 1.04 real, 1.04 cpu
  seconds
  MSG(Jan 20 23:25:44): Rerunning proof of Body_Assert_eta_TCC1
  MSG(Jan 20 23:25:44): Body_Assert_eta_TCC1 proved in 0.76 real, 0.76 cpu
  seconds
  MSG(Jan 20 23:25:44): Rerunning proof of Body_Assert_eta_TCC2
  MSG(Jan 20 23:25:45): Body_Assert_eta_TCC2 unproved in 1.08 real, 1.08 cpu
  seconds
  
  That is, there are some unfinished TCCs in body_adt (which is generated
  automatically).
  
  ------=_Part_8877_29820388.1200871678045
  Content-Type: text/html; charset=ISO-8859-1
  Content-Transfer-Encoding: 7bit
  Content-Disposition: inline
  
  Hi,<br><br>When running the proof of our specification, on the PVS Status buf
 fer we get:<br><br>Grand Totals: 502 proofs, 502 attempted, 502 succeeded (205
 3.33 s)<br><br>However, the PVS Log buffer says:<br><br>MSG(Jan 21 00:01:00): 
 CorrectnessAnnProgram: 520 proofs attempted, 512 proved in 
  2069.89 real, 2069.89 cpu seconds<br><br>I found some messages like:<br><br>M
 SG(Jan 20 23:25:28): Body_Plus_eta_TCC2 unproved in 1.05 real, 1.05 cpu second
 s<br>MSG(Jan 20 23:25:28): Rerunning proof of Body_Plus_eta_TCC3<br>
  MSG(Jan 20 23:25:29): Body_Plus_eta_TCC3 unproved in 1.01 real, 1.01 cpu seco
 nds<br>MSG(Jan 20 23:25:29): Rerunning proof of Body_Conj_eta_TCC1<br>MSG(Jan 
 20 23:25:29): Body_Conj_eta_TCC1 proved in 0.79 real, 0.79 cpu seconds
  <br>MSG(Jan 20 23:25:30): Rerunning proof of Body_Conj_eta_TCC2<br>MSG(Jan 20
  23:25:37): Body_Conj_eta_TCC2 unproved in 1.18 real, 1.18 cpu seconds<br>MSG(
 Jan 20 23:25:37): Rerunning proof of Body_Conj_eta_TCC3<br>MSG(Jan 20 23:25:38
 ): Body_Conj_eta_TCC3 unproved in 
  1.15 real, 1.15 cpu seconds<br>MSG(Jan 20 23:25:38): Rerunning proof of Body_
 Eq_eta_TCC1<br>MSG(Jan 20 23:25:39): Body_Eq_eta_TCC1 proved in 0.80 real, 0.8
 0 cpu seconds<br>MSG(Jan 20 23:25:39): Rerunning proof of Body_Eq_eta_TCC2
  <br>MSG(Jan 20 23:25:40): Body_Eq_eta_TCC2 unproved in 1.18 real, 1.18 cpu se
 conds<br>MSG(Jan 20 23:25:40): Rerunning proof of Body_Eq_eta_TCC3<br>MSG(Jan 
 20 23:25:41): Body_Eq_eta_TCC3 unproved in 1.09 real, 1.09 cpu seconds
  <br>MSG(Jan 20 23:25:42): Rerunning proof of Body_StmtExpr_eta_TCC1<br>MSG(Ja
 n 20 23:25:42): Body_StmtExpr_eta_TCC1 proved in 0.77 real, 0.77 cpu seconds<b
 r>MSG(Jan 20 23:25:42): Rerunning proof of Body_StmtExpr_eta_TCC2<br>
  MSG(Jan 20 23:25:43): Body_StmtExpr_eta_TCC2 unproved in 1.04 real, 1.04 cpu 
 seconds<br>MSG(Jan 20 23:25:44): Rerunning proof of Body_Assert_eta_TCC1<br>MS
 G(Jan 20 23:25:44): Body_Assert_eta_TCC1 proved in 0.76 real, 0.76
   cpu seconds<br>MSG(Jan 20 23:25:44): Rerunning proof of Body_Assert_eta_TCC2
 <br>MSG(Jan 20 23:25:45): Body_Assert_eta_TCC2 unproved in 1.08 real, 1.08 cpu
  seconds<br><br>That is, there are some unfinished TCCs in body_adt (which is 
 generated automatically).
  <br>
  
  ------=_Part_8877_29820388.1200871678045--

How-To-Repeat: 

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