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

PVS Bug 1081


Synopsis:        [PVS-Help] An error when pvs generates tcc's
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Wed Oct 26 00:30:00 -0700 2011
Originator:      =?iso-8859-1?Q?Thiago_Mendon=E7a_Ferreira_Ramos?=
Release:         PVS 5.0
Organization:    yahoo.com.br
Environment: 
 System:          
 Architecture: 

Description: 
  ---1375862948-1890024300-1319568724=:28895
  Content-Type: text/plain; charset=iso-8859-1
  Content-Transfer-Encoding: quoted-printable
  
  Hi Sam,=0A=0AActually, I am not right about that, but I thing that it is no=
  t a bug because Dr Ayala e I could find the error at now.=0A=0AHowever, pvs=
   cannot say where the mistake is.=0A=0AOur specs before:=0A________________=
  _________________________________=0A=0Aoperator : TYPE =3D [cryptType + sig=
  nedType + anonymous]=0A=0AopStamp : TYPE =3D [op + opSigned + anonymous]=0A=
  =0AopUserLess :=A0 TYPE (IN?_1)=0A=0A______________________________________=
  ______________=0A=0A=0AOur specs after the corrections:=0A_________________=
  ____________________________________________=0A=0Aoperator : TYPE =3D [cryp=
  tType + signedType + anonymous]=0A=0AopStamp : TYPE =3D [op + opSigned + an=
  onymous]=0A=0A=A0opUserLess?(op1 : opStamp) : bool =3D IN?_1(op1)=0A=0A=0Ao=
  pUserLess :=A0 TYPE (opUserLess?)=0A=0A%Where types in sum op types were de=
  fined in file.=0A=0A_______________________________________________________=
  _____=0A=0AThanks, I really apreciate it,=0A=0A=0AThiago=0A=0A=0A__________=
  ______________________=0ADe: Sam Owre <owre@csl.sri.com>=0APara: =3D?iso-88=
  59-1?Q?Thiago_Mendon=3DE7a_Ferreira_Ramos?=3D <thiagomendoncaferreiraramos@=
  yahoo.com.br>=0ACc: "pvs-help@csl.sri.com" <pvs-help@csl.sri.com>; "ayala@u=
  nb.br" <ayala@unb.br>=0AEnviadas: Ter=E7a-feira, 25 de Outubro de 2011 16:2=
  4=0AAssunto: Re: [PVS-Help] An error when pvs generates tcc's=0A=0AHi Thiag=
  o,=0A=0AIt looks like you found a bug - could you send me your specs so I c=
  an=0Aanalyze it?=0A=0AThanks,=0ASam Owre=0A=0AThiago Mendon=E7a Ferreira Ra=
  mos wrote:=0A=0A> Hi,=0A> =0A> I am trying generate tcc's in pvs. However, =
  it appears an error message:=0A> =0A> "Error: the assertion (and resolution=
  s (null (cdr resolutions))) failed."=0A> =0A> Unfortunatily, I do not know =
  how solve this problem.=0A> =0A> Could you help me, please?
  ---1375862948-1890024300-1319568724=:28895
  Content-Type: text/html; charset=iso-8859-1
  Content-Transfer-Encoding: quoted-printable
  
  <html><body><div style=3D"color:#000; background-color:#fff; font-family:ti=
  mes new roman, new york, times, serif;font-size:12pt"><div><span>Hi Sam,</s=
  pan></div><div><br><span></span></div><div><span>Actually, I am not right a=
  bout that, but I thing that it is not a bug because Dr Ayala e I could find=
   the error at now.</span></div><div><br><span></span></div><div><span>Howev=
  er, pvs cannot say where the mistake is.</span></div><div><br><span></span>=
  </div><div><span>Our specs before:</span></div><div>_______________________=
  __________________________<br><span></span></div><div><span>operator : TYPE=
   =3D [cryptType + signedType + anonymous]<br><br>opStamp : TYPE =3D [op + o=
  pSigned + anonymous]</span></div><div><br><span></span></div><div><span>opU=
  serLess :&nbsp; TYPE (IN?_1)</span></div><div>_____________________________=
  _______________________<br></div><div><br></div><div>Our specs after the
   corrections:</div><div>___________________________________________________=
  __________<br></div><div><span>operator : TYPE =3D [cryptType + signedType =
  + anonymous]<br>=0A    <br>=0AopStamp : TYPE =3D [op + opSigned + anonymous=
  ]</span></div><div><br><span></span></div><div><span>&nbsp;opUserLess?(op1 =
  : opStamp) : bool =3D IN?_1(op1)<br></span></div>=0A<div><br>=0A  <span></s=
  pan></div>=0A<div><span>opUserLess :&nbsp; TYPE (opUserLess?)</span></div><=
  div><br><span></span></div><div><span>%Where types in sum op types were def=
  ined in file.<br></span></div><div>________________________________________=
  ____________________</div><div><br></div><div>Thanks, I really apreciate it=
  ,<br></div><div><br></div><div>Thiago<br></div><div style=3D"font-family: t=
  imes new roman, new york, times, serif; font-size: 12pt;"><div style=3D"fon=
  t-family: times new roman, new york, times, serif; font-size: 12pt;"><font =
  face=3D"Arial" size=3D"2"><hr size=3D"1"><b><span style=3D"font-weight:bold=
  ;">De:</span></b> Sam Owre &lt;owre@csl.sri.com&gt;<br><b><span style=3D"fo=
  nt-weight: bold;">Para:</span></b> =3D?iso-8859-1?Q?Thiago_Mendon=3DE7a_Fer=
  reira_Ramos?=3D &lt;thiagomendoncaferreiraramos@yahoo.com.br&gt;<br><b><spa=
  n style=3D"font-weight: bold;">Cc:</span></b> "pvs-help@csl.sri.com" &lt;pv=
  s-help@csl.sri.com&gt;; "ayala@unb.br" &lt;ayala@unb.br&gt;<br><b><span sty=
  le=3D"font-weight:
   bold;">Enviadas:</span></b> Ter=E7a-feira, 25 de Outubro de 2011 16:24<br>=
  <b><span style=3D"font-weight: bold;">Assunto:</span></b> Re: [PVS-Help] An=
   error when pvs generates tcc's<br></font><br>Hi Thiago,<br><br>It looks li=
  ke you found a bug - could you send me your specs so I can<br>analyze it?<b=
  r><br>Thanks,<br>Sam Owre<br><br>Thiago Mendon=E7a Ferreira Ramos wrote:<br=
  ><br>&gt; Hi,<br>&gt; <br>&gt; I am trying generate tcc's in pvs. However, =
  it appears an error message:<br>&gt; <br>&gt; "Error: the assertion (and re=
  solutions (null (cdr resolutions))) failed."<br>&gt; <br>&gt; Unfortunatily=
  , I do not know how solve this problem.<br>&gt; <br>&gt; Could you help me,=
   please?<br><br><br></div></div></div></body></html>
  ---1375862948-1890024300-1319568724=:28895--

How-To-Repeat: 

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