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