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

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