--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on August 2014 ---
[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