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]

[Frama-c-discuss] memory allocation + pointers

Oups.. Right question for wrong code. Sorry about it.
Here is the right one (with no assigns clause).
Could you please give me some indications about the right assigns clause
for this function?

========================================
int *d, *b;
/*@ requires \valid(a) &&
  @ \valid(b) &&
  @ \valid(d) &&
  @ \valid(a+(0..4)) &&
  @ \valid(b+(a[0]..a[4])) &&
  @  \base_addr(a) != \base_addr(b);

  @ ensures a[0] == (\at(a[0], Pre) ^ (\at(b[a[3]],Pre)^\at(d[i],Pre)));
  @ ensures a[1] == (\at(a[1], Pre) ^ (\at(b[\at(a[4],Pre)],Pre)));
*/

void test3 (int *a, int i)
{
a[0] ^= b[a[3]] ^ d[i];
 a[1] ^= b[a[4]];
}


2014-08-09 7:14 GMT+00:00 Guillaume Melquiond <guillaume.melquiond at inria.fr>
:

> On 08/08/2014 12:48, Maria Christofi wrote:
>
>  I have a problem with the code below.
>> I want to prove the two postconditions with the Jessie plugin, but it
>> doesn't seem possible..
>>
>
> Since you code performs xor assignments while your postconditions state
> that it performs additive assignments, the failure seems sensible. After
> changing "^=" into "+=" in the code, the two postconditions are instantly
> verified.
>
> That said, there are a lot of things left to prove. For instance, that
> only "*a" is assigned, which is wrong. And that a[0], a[1], a[4] are valid
> cells, which is impossible to prove. And that b[3] and b[a[4]] are valid
> cells, which is also impossible to prove. So there are quite a few things
> to add or to change in the specification.
>
> Best regards,
>
> Guillaume
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>



-- 
Maria Christofi
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140809/f5645a75/attachment.html>