# 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.

# No subject

```write on the same memory location and to prove something about it.
(Please correct me if I am wrong)

I have an annotated algorithm that is proven:

/*@
requires 0 <=3D length;
requires \valid_range (a, 0, length-1);
requires \valid_range (b, 0, length-1);

ensures \result =3D=3D length;
ensures \forall integer k; 0 <=3D k < length =3D=3D>
(a[k] =3D=3D old_value =3D=3D>        b[k] =3D=3D new_value);
ensures \forall integer k; 0 <=3D k < length =3D=3D>
(a[k] !=3D old_value =3D=3D>        b[k] =3D=3D a[k]);

*/
int replace_copy_array (int* a, int length, int* b, int old_value, =
int new_value )
{
int i =3D 0;
/*@
loop invariant 0 <=3D i <=3D length;

loop invariant \forall integer k; 0 <=3D k < i =3D=3D>
(a[k] =3D=3D old_value =3D=3D>
b[k] =3D=3D new_value);

loop invariant \forall integer k; 0 <=3D k < i =3D=3D>
(a[k] !=3D old_value =3D=3D>
b[k] =3D=3D a[k]);

*/
for (; i !=3D length; ++i)
{
if (a[i]=3D=3Dold_value)
b[i] =3D new_value;
else
b[i] =3D a[i];
}
return i;
}

And I have a similar algorithm but this one does not copy the result:

/*@
requires 0 <=3D length;
requires \valid_range (a, 0, length-1);

ensures \forall integer k;
0 <=3D k < length =3D=3D>
(\old(a[k]) =3D=3D old_value =3D=3D>
a[k]=3D=3D new_value);
*/
void replace_array (int* a, int length, int old_value, int new_value =
)
{
int i =3D 0;
/*@
loop invariant 0  <=3D i <=3D length;

loop invariant \forall integer k;  0 <=3D k < i =3D=3D>
(\at(a[k],Pre) =3D=3D old_value =3D=3D>
a[k] =3D=3D new_value);  =20
*/
for (; i !=3D length; ++i)
{
if (a[i] =3D=3D old_value)
{
a[i] =3D new_value;
}
}
}

I would like to know, what I have missed.

Thank you for the help,
Cheers

Christoph
------=_NextPart_000_0024_01C99022.B46167A0
Content-Type: text/html;
charset="iso-8859-1"
Content-Transfer-Encoding: quoted-printable

<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
<META http-equiv=3DContent-Type content=3D"text/html; =
charset=3Diso-8859-1">
<META content=3D"MSHTML 6.00.6001.18203" name=3DGENERATOR>
<STYLE></STYLE>
<BODY bgColor=3D#ffffff>
<DIV><FONT face=3DArial size=3D2>Hello,</FONT></DIV>
<DIV><FONT face=3DArial size=3D2></FONT>&nbsp;</DIV>
<DIV><FONT face=3DArial size=3D2>I am trying to explore the limitations =
of proving=20
with Jessie.</FONT></DIV>
<DIV><FONT face=3DArial size=3D2></FONT>&nbsp;</DIV>
<DIV><FONT face=3DArial size=3D2>From what I understood of the recent =
mails, it is=20
difficult to read and write on the same memory location and to prove =
something=20
<DIV><FONT face=3DArial size=3D2>(Please correct me if I am =
wrong)</FONT></DIV>
<DIV><FONT face=3DArial size=3D2></FONT>&nbsp;</DIV>
<DIV><FONT face=3DArial size=3D2>I have an annotated algorithm that is=20
proven:</FONT></DIV>
<DIV><FONT face=3DArial size=3D2></FONT>&nbsp;</DIV>
<DIV><FONT face=3DArial size=3D2>&nbsp;/*@<BR>&nbsp;&nbsp;&nbsp;&nbsp; =
requires 0=20
&lt;=3D length;<BR>&nbsp;&nbsp;&nbsp;&nbsp; requires \valid_range (a, 0, =

length-1);<BR>&nbsp;&nbsp;&nbsp;&nbsp; requires \valid_range (b, 0,=20
length-1);</FONT></DIV><FONT face=3DArial size=3D2>
<DIV><BR>&nbsp;&nbsp;&nbsp;&nbsp; ensures \result =3D=3D=20
length;<BR>&nbsp;&nbsp;&nbsp;&nbsp; ensures \forall integer k; 0 &lt;=3D =
k &lt;=20
length =3D=3D&gt;<BR>&nbsp;&nbsp;&nbsp;&nbsp; (a[k] =3D=3D old_value=20
=3D=3D&gt;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; b[k] =3D=3D=20
new_value);<BR>&nbsp;&nbsp;&nbsp;&nbsp; ensures \forall integer k; 0 =
&lt;=3D k=20
&lt; length =3D=3D&gt;<BR>&nbsp;&nbsp;&nbsp;&nbsp; (a[k] !=3D old_value=20
=3D=3D&gt;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; b[k] =3D=3D =
a[k]);</DIV>
<DIV>&nbsp;</DIV>
<DIV>&nbsp;&nbsp;&nbsp; */<BR>&nbsp;&nbsp;&nbsp; int replace_copy_array =
(int* a,=20
int length, int* b, int old_value, int new_value =
)<BR>{<BR>&nbsp;&nbsp;&nbsp;=20
int i =3D 0;<BR>&nbsp;&nbsp;&nbsp; /*@<BR>&nbsp;&nbsp;&nbsp;&nbsp; loop =
invariant=20
0 &lt;=3D i &lt;=3D length;</DIV>
<DIV>&nbsp;</DIV>
<DIV>&nbsp;&nbsp;&nbsp;&nbsp; loop invariant \forall integer k; 0 =
&lt;=3D k &lt; i=20
=3D=3D&gt;<BR>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;  (a[k] =3D=3D =
old_value=20
=3D=3D&gt;<BR>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;  b[k] =3D=3D =
new_value);</DIV>
<DIV>&nbsp;</DIV>
<DIV>&nbsp;&nbsp;&nbsp; loop invariant \forall integer k; 0 &lt;=3D k =
&lt; i=20
=3D=3D&gt;<BR>&nbsp;&nbsp;&nbsp; (a[k] !=3D old_value =
=3D=3D&gt;<BR>&nbsp;&nbsp;&nbsp;=20
b[k] =3D=3D a[k]);</DIV>
<DIV><BR>&nbsp;&nbsp;&nbsp; */<BR>&nbsp;&nbsp;&nbsp; for (; i !=3D =
length;=20
++i)<BR>&nbsp;&nbsp;&nbsp; =
{<BR>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; if=20
(a[i]=3D=3Dold_value)<BR>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;=
&nbsp;&nbsp;&nbsp;=20
b[i] =3D new_value;<BR>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;=20
else<BR>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp=
; b[i]=20
=3D a[i];<BR>&nbsp;&nbsp;&nbsp; }<BR>&nbsp;&nbsp;&nbsp; return =
i;<BR>}</DIV>
<DIV>&nbsp;</DIV>
<DIV>And I have a similar algorithm but this one does not copy the =
result:</DIV>
<DIV>&nbsp;</DIV>
<DIV>/*@<BR>&nbsp;&nbsp;&nbsp;&nbsp; requires 0 &lt;=3D=20
length;<BR>&nbsp;&nbsp;&nbsp;&nbsp; requires \valid_range (a, 0,=20
length-1);</DIV>
<DIV>&nbsp;</DIV>
<DIV>&nbsp;&nbsp;&nbsp;&nbsp; ensures \forall integer=20
k;<BR>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; 0 &lt;=3D k &lt; =
length=20
=3D=3D&gt;<BR>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; =
(\old(a[k]) =3D=3D=20
old_value =3D=3D&gt;<BR>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; a[k]=3D=3D=20
new_value);<BR>&nbsp;&nbsp;&nbsp; */<BR>&nbsp;&nbsp;&nbsp; void =
replace_array=20
(int* a, int length, int old_value, int new_value =
)<BR>{<BR>&nbsp;&nbsp;&nbsp;=20
int i =3D 0;<BR>&nbsp;&nbsp;&nbsp; /*@<BR>&nbsp;&nbsp;&nbsp;&nbsp; loop =
invariant=20
0&nbsp; &lt;=3D i &lt;=3D length;</DIV>
<DIV>&nbsp;</DIV>
<DIV>&nbsp;&nbsp;&nbsp;&nbsp; loop invariant \forall integer k;&nbsp; 0 =
&lt;=3D k=20
&lt; i =3D=3D&gt;<BR>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; (\at(a[k],Pre) =
=3D=3D=20
old_value =3D=3D&gt;<BR>&nbsp;&nbsp;&nbsp;&nbsp; &nbsp;&nbsp;a[k] =3D=3D =

new_value);&nbsp;&nbsp;&nbsp;<BR>&nbsp;&nbsp;&nbsp; =
*/<BR>&nbsp;&nbsp;&nbsp; for=20
(; i !=3D length; ++i)<BR>&nbsp;&nbsp;&nbsp;=20
{<BR>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; if (a[i] =3D=3D=20
old_value)<BR>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;=20
{<BR>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; =
a[i] =3D=20
new_value;<BR>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; }</DIV>
<DIV>&nbsp;&nbsp;&nbsp; }<BR>}<BR></DIV>
<DIV>I would like to know, what I have missed.</DIV>
<DIV>&nbsp;</DIV>
<DIV>Thank you&nbsp;for the help,</DIV>
<DIV>Cheers</DIV>
<DIV>&nbsp;</DIV>
<DIV>Christoph</DIV></FONT></BODY></HTML>

------=_NextPart_000_0024_01C99022.B46167A0--

```