--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on December 2008 ---
=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--