Frama-C-discuss mailing list archives
This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
No subject
- Subject: No subject
- From: bogus@does.not.exist.com ()
- Date: Mon, 08 Dec 2008 18:11:52 -0000
=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> </o:p></p>
<p class=3DMsoNormal>Hi everyone!<o:p></o:p></p>
<p class=3DMsoNormal><o:p> </o:p></p>
<p class=3DMsoNormal>From this code: <o:p></o:p></p>
<p class=3DMsoNormal><o:p> </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'> @*/</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> </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'>
</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'>
</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'>
a[1] =3D((x+1)&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'>
a[2] =3D((x+y)&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> </o:p></span></p>
<p class=3DMsoNormal><span lang=3DEN-US>And part of the generated =
code for
Jessie is the following:<o:p></o:p></span></p>
<p class=3DMsoNormal><span lang=3DEN-US><o:p> </o:p></span></p>
<p class=3DMsoNormal><span lang=3DEN-US>….<o:p></o:p></span></p>
<p class=3DMsoNormal><span lang=3DEN-US> </span>(var int8 =
x_0);<o:p></o:p></p>
<p class=3DMsoNormal> (C_44 : (x_0 =3D (C_43 : (C_42 : (a +
0)).char_M)));<o:p></o:p></p>
<p class=3DMsoNormal> <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> =
((C_47 : ( (C_46 : ((C_45 : (x_0 :> int32)) + 1)) :> int32)) =
&
255)) :> int8))));<o:p></o:p></span></p>
<p class=3DMsoNormal><span lang=3DEN-US> =
(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> =
((C_56 : (<o:p></o:p></span></p>
<p class=3DMsoNormal><span =
lang=3DEN-US> =
(C_55 : ((C_54 : (x_0 :> int32)) + (C_53 : (y :>
int32)))) :> int32)) & 255)) :> =
int8))));<o:p></o:p></span></p>
<p class=3DMsoNormal><span lang=3DEN-US> =
<o:p></o:p></span></p>
<p class=3DMsoNormal><span lang=3DEN-US> … =
<o:p></o:p></span></p>
<p class=3DMsoNormal><span lang=3DEN-US> =
<o:p></o:p></span></p>
<p class=3DMsoNormal><span lang=3DEN-US>I realized that the =
“x” declaration
does not correspond to the type that is declared in C, and =
I’m wondering
why this happens.<o:p></o:p></span></p>
<p class=3DMsoNormal><span lang=3DEN-US><o:p> </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 ((x+1)&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> </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…127.<o:p></o:p></span></p>
<p class=3DMsoNormal><span lang=3DEN-US><o:p> </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> <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> </o:p></span></p>
<p class=3DMsoNormal><span lang=3DEN-US><o:p> </o:p></span></p>
</div>
</body>
</html>
------=_NextPart_000_00FD_01C95C68.6357EA70--
- Prev by Date: [Frama-c-discuss] jessie questions
- Next by Date: [Frama-c-discuss] interfacing non-OCaml programs with Frama-C
- Previous by thread: [Frama-c-discuss] jessie questions
- Next by thread: No subject
- Index(es):