--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on December 2008 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

No subject



=20

/*@ requires \valid(a+(0..10));

  @*/

void g(unsigned char *a,unsigned char y){

=20

      unsigned char x =3D a[0];

     =20

      a[1] =3D((x+1)&0xff);

      a[2] =3D((x+y)&0xff);

}

=20

And part of the  generated code for Jessie is the following:

=20

=85.

   (var int8 x_0);

   (C_44 : (x_0 =3D (C_43 : (C_42 : (a + 0)).char_M)));

      (C_52 : ((C_51 : (C_50 : (a + 1)).char_M) =3D (C_49 : ((C_48 :=20

                    ((C_47 : ( (C_46 : ((C_45 : (x_0 :> int32)) + 1)) :>
int32)) & 255)) :> int8))));

      (C_61 : ((C_60 : (C_59 : (a + 2)).char_M) =3D (C_58 : ((C_57 :

                    ((C_56 : (

                     (C_55 : ((C_54 : (x_0 :> int32)) + (C_53 : (y :>
int32)))) :> int32)) & 255)) :> int8))));

     =20

 =85  =20

  =20

I realized that the =93x=94 declaration  does not correspond to the type =
that is
declared in C, and I=92m wondering why this happens.

=20

To prove the safety conditions, I added some axioms to validate the =
ranges
of bitwise operations. However the generated proof obligations are not
provable with my axioms, because it tries to validate that the range of
((x+1)&0xff) is between -127 and 127, and it is between 0 and 255.=20

=20

I manually changed the code and substitute all the int8 and int32 for =
uint8,
but there is still some proof obligations that tries to validate that =
the
range is between -127=85127.

=20

What can I do to solve this problem?

=20

Best regards,

B=E1rbara=20

=20

=20


------=_NextPart_000_00FD_01C95C68.6357EA70
Content-Type: text/html;
	charset="iso-8859-1"
Content-Transfer-Encoding: quoted-printable

<META HTTP-EQUIV=3D"Content-Type" CONTENT=3D"text/html; =
charset=3Diso-8859-1">
<html xmlns:v=3D"urn:schemas-microsoft-com:vml" =
xmlns:o=3D"urn:schemas-microsoft-com:office:office" =
xmlns:w=3D"urn:schemas-microsoft-com:office:word" =
xmlns:m=3D"http://schemas.microsoft.com/office/2004/12/omml"; =
xmlns=3D"http://www.w3.org/TR/REC-html40";>

<head>

<meta name=3DGenerator content=3D"Microsoft Word 12 (filtered medium)">
<style>
<!--
 /* Font Definitions */
 @font-face
	{font-family:"Cambria Math";
	panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
	{font-family:Calibri;
	panose-1:2 15 5 2 2 2 4 3 2 4;}
 /* Style Definitions */
 p.MsoNormal, li.MsoNormal, div.MsoNormal
	{margin:0cm;
	margin-bottom:.0001pt;
	font-size:11.0pt;
	font-family:"Calibri","sans-serif";}
a:link, span.MsoHyperlink
	{mso-style-priority:99;
	color:blue;
	text-decoration:underline;}
a:visited, span.MsoHyperlinkFollowed
	{mso-style-priority:99;
	color:purple;
	text-decoration:underline;}
span.EmailStyle17
	{mso-style-type:personal;
	font-family:"Calibri","sans-serif";
	color:windowtext;}
span.EmailStyle18
	{mso-style-type:personal-reply;
	font-family:"Calibri","sans-serif";
	color:#1F497D;}
.MsoChpDefault
	{mso-style-type:export-only;
	font-size:10.0pt;}
@page Section1
	{size:612.0pt 792.0pt;
	margin:70.85pt 3.0cm 70.85pt 3.0cm;}
div.Section1
	{page:Section1;}
-->
</style>
<!--[if gte mso 9]><xml>
 <o:shapedefaults v:ext=3D"edit" spidmax=3D"1026" />
</xml><![endif]--><!--[if gte mso 9]><xml>
 <o:shapelayout v:ext=3D"edit">
  <o:idmap v:ext=3D"edit" data=3D"1" />
 </o:shapelayout></xml><![endif]-->
</head>

<body lang=3DPT link=3Dblue vlink=3Dpurple>

<div class=3DSection1>

<p class=3DMsoNormal><o:p>&nbsp;</o:p></p>

<p class=3DMsoNormal>Hi everyone!<o:p></o:p></p>

<p class=3DMsoNormal><o:p>&nbsp;</o:p></p>

<p class=3DMsoNormal>From this code: <o:p></o:p></p>

<p class=3DMsoNormal><o:p>&nbsp;</o:p></p>

<p class=3DMsoNormal style=3D'text-autospace:none'><span lang=3DEN-US
style=3D'font-size:10.0pt;font-family:"Courier New";color:royalblue'>/*@ =
</span><b><span
lang=3DEN-US style=3D'font-size:10.0pt;font-family:"Courier =
New";color:midnightblue'>requires</span></b><span
lang=3DEN-US style=3D'font-size:10.0pt;font-family:"Courier =
New";color:royalblue'> </span><b><span
lang=3DEN-US style=3D'font-size:10.0pt;font-family:"Courier =
New";color:blue'>\valid</span></b><span
lang=3DEN-US style=3D'font-size:10.0pt;font-family:"Courier =
New";color:royalblue'>(a+(0..10));</span><span
lang=3DEN-US style=3D'font-size:10.0pt;font-family:"Courier =
New"'><o:p></o:p></span></p>

<p class=3DMsoNormal style=3D'text-autospace:none'><span lang=3DEN-US
style=3D'font-size:10.0pt;font-family:"Courier =
New";color:royalblue'>&nbsp; @*/</span><span
lang=3DEN-US style=3D'font-size:10.0pt;font-family:"Courier =
New"'><o:p></o:p></span></p>

<p class=3DMsoNormal style=3D'text-autospace:none'><b><span lang=3DEN-US
style=3D'font-size:10.0pt;font-family:"Courier =
New";color:#7F0055'>void</span></b><span
lang=3DEN-US style=3D'font-size:10.0pt;font-family:"Courier =
New";color:black'> g(</span><b><span
lang=3DEN-US style=3D'font-size:10.0pt;font-family:"Courier =
New";color:#7F0055'>unsigned</span></b><span
lang=3DEN-US style=3D'font-size:10.0pt;font-family:"Courier =
New";color:black'> </span><b><span
lang=3DEN-US style=3D'font-size:10.0pt;font-family:"Courier =
New";color:#7F0055'>char</span></b><span
lang=3DEN-US style=3D'font-size:10.0pt;font-family:"Courier =
New";color:black'> *a,</span><b><span
lang=3DEN-US style=3D'font-size:10.0pt;font-family:"Courier =
New";color:#7F0055'>unsigned</span></b><span
lang=3DEN-US style=3D'font-size:10.0pt;font-family:"Courier =
New";color:black'> </span><b><span
lang=3DEN-US style=3D'font-size:10.0pt;font-family:"Courier =
New";color:#7F0055'>char</span></b><span
lang=3DEN-US style=3D'font-size:10.0pt;font-family:"Courier =
New";color:black'> y){</span><span
lang=3DEN-US style=3D'font-size:10.0pt;font-family:"Courier =
New"'><o:p></o:p></span></p>

<p class=3DMsoNormal style=3D'text-autospace:none'><span lang=3DEN-US
style=3D'font-size:10.0pt;font-family:"Courier =
New"'><o:p>&nbsp;</o:p></span></p>

<p class=3DMsoNormal style=3D'text-autospace:none'><span lang=3DEN-US
style=3D'font-size:10.0pt;font-family:"Courier =
New";color:black'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
</span><b><span lang=3DEN-US =
style=3D'font-size:10.0pt;font-family:"Courier New";
color:#7F0055'>unsigned</span></b><span lang=3DEN-US =
style=3D'font-size:10.0pt;
font-family:"Courier New";color:black'> </span><b><span lang=3DEN-US
style=3D'font-size:10.0pt;font-family:"Courier =
New";color:#7F0055'>char</span></b><span
lang=3DEN-US style=3D'font-size:10.0pt;font-family:"Courier =
New";color:black'> x =3D
a[0];</span><span lang=3DEN-US =
style=3D'font-size:10.0pt;font-family:"Courier =
New"'><o:p></o:p></span></p>

<p class=3DMsoNormal style=3D'text-autospace:none'><span lang=3DEN-US
style=3D'font-size:10.0pt;font-family:"Courier =
New";color:black'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
</span><span lang=3DEN-US style=3D'font-size:10.0pt;font-family:"Courier =
New"'><o:p></o:p></span></p>

<p class=3DMsoNormal style=3D'text-autospace:none'><span lang=3DEN-US
style=3D'font-size:10.0pt;font-family:"Courier =
New";color:black'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
a[1] =3D((x+1)&amp;0xff);</span><span lang=3DEN-US =
style=3D'font-size:10.0pt;
font-family:"Courier New"'><o:p></o:p></span></p>

<p class=3DMsoNormal style=3D'text-autospace:none'><span lang=3DEN-US
style=3D'font-size:10.0pt;font-family:"Courier =
New";color:black'>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
a[2] =3D((x+y)&amp;0xff);</span><span lang=3DEN-US =
style=3D'font-size:10.0pt;
font-family:"Courier New"'><o:p></o:p></span></p>

<p class=3DMsoNormal><span lang=3DEN-US =
style=3D'font-size:10.0pt;font-family:"Courier New";
color:black'>}</span><span lang=3DEN-US><o:p></o:p></span></p>

<p class=3DMsoNormal><span lang=3DEN-US><o:p>&nbsp;</o:p></span></p>

<p class=3DMsoNormal><span lang=3DEN-US>And part of the &nbsp;generated =
code for
Jessie is the following:<o:p></o:p></span></p>

<p class=3DMsoNormal><span lang=3DEN-US><o:p>&nbsp;</o:p></span></p>

<p class=3DMsoNormal><span lang=3DEN-US>&#8230;.<o:p></o:p></span></p>

<p class=3DMsoNormal><span lang=3DEN-US>&nbsp;&nbsp; </span>(var int8 =
x_0);<o:p></o:p></p>

<p class=3DMsoNormal>&nbsp; &nbsp;(C_44 : (x_0 =3D (C_43 : (C_42 : (a +
0)).char_M)));<o:p></o:p></p>

<p class=3DMsoNormal>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; <span =
lang=3DEN-US>(C_52 :
((C_51 : (C_50 : (a + 1)).char_M) =3D (C_49 : ((C_48 : =
</span><o:p></o:p></p>

<p class=3DMsoNormal><span =
lang=3DEN-US>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;=
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
&nbsp;((C_47 : ( (C_46 : ((C_45 : (x_0 :&gt; int32)) + 1)) :&gt; int32)) =
&amp;
255)) :&gt; int8))));<o:p></o:p></span></p>

<p class=3DMsoNormal><span lang=3DEN-US>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; =
(C_61 :
((C_60 : (C_59 : (a + 2)).char_M) =3D (C_58 : ((C_57 =
:<o:p></o:p></span></p>

<p class=3DMsoNormal><span =
lang=3DEN-US>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;=
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
&nbsp;((C_56 : (<o:p></o:p></span></p>

<p class=3DMsoNormal><span =
lang=3DEN-US>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;=
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
&nbsp;&nbsp;&nbsp;(C_55 : ((C_54 : (x_0 :&gt; int32)) + (C_53 : (y :&gt;
int32)))) :&gt; int32)) &amp; 255)) :&gt; =
int8))));<o:p></o:p></span></p>

<p class=3DMsoNormal><span lang=3DEN-US>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; =
<o:p></o:p></span></p>

<p class=3DMsoNormal><span lang=3DEN-US>&nbsp;&#8230;&nbsp;&nbsp; =
<o:p></o:p></span></p>

<p class=3DMsoNormal><span lang=3DEN-US>&nbsp;&nbsp; =
<o:p></o:p></span></p>

<p class=3DMsoNormal><span lang=3DEN-US>I realized that the =
&#8220;x&#8221; declaration
&nbsp;does not correspond to the type that is declared in C, and =
I&#8217;m wondering
why this happens.<o:p></o:p></span></p>

<p class=3DMsoNormal><span lang=3DEN-US><o:p>&nbsp;</o:p></span></p>

<p class=3DMsoNormal><span lang=3DEN-US>To prove the safety conditions, =
I added
some axioms to validate the ranges of bitwise operations. However the =
generated
proof obligations are not provable with my axioms, because it tries to =
validate
that the range of &nbsp;((x+1)&amp;0xff) is between -127 and 127, and it =
is
between 0 and 255. <o:p></o:p></span></p>

<p class=3DMsoNormal><span lang=3DEN-US><o:p>&nbsp;</o:p></span></p>

<p class=3DMsoNormal><span lang=3DEN-US>I manually changed the code and =
substitute
all the int8 and int32 for uint8, but there is still some proof =
obligations
that tries to validate that the range is between =
-127&#8230;127.<o:p></o:p></span></p>

<p class=3DMsoNormal><span lang=3DEN-US><o:p>&nbsp;</o:p></span></p>

<p class=3DMsoNormal><span lang=3DEN-US>What can I do to solve this =
problem?<o:p></o:p></span></p>

<p class=3DMsoNormal><span lang=3DEN-US>&nbsp;<o:p></o:p></span></p>

<p class=3DMsoNormal><span lang=3DEN-US>Best =
regards,<o:p></o:p></span></p>

<p class=3DMsoNormal><span lang=3DEN-US>B=E1rbara <o:p></o:p></span></p>

<p class=3DMsoNormal><span lang=3DEN-US><o:p>&nbsp;</o:p></span></p>

<p class=3DMsoNormal><span lang=3DEN-US><o:p>&nbsp;</o:p></span></p>

</div>

</body>

</html>

------=_NextPart_000_00FD_01C95C68.6357EA70--