--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on August 2014 ---
Good morning, 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.. I think that what's missing is something saying that only a[0] changes in the first instruction and only a[1] in the second one (every a[i] except the one concerned stays unchanged). Am I right? Is it possible? Have an nice evening! Maria ============================================================= int *d, *b; /*@ requires \valid(a) && @ \valid(b) && @ \base_addr(a) != \base_addr(b); @ assigns *a; @ ensures a[0] == (\at(a[0],Pre)+\at(b[3],Pre)); @ ensures a[1] == (\at(a[1],Pre)+\at(b[\at(a[4],Pre)],Pre)); */ void test (int *a, int i) { a[0] ^= b[3] a[1] ^= b[a[4]]; } -- Maria Christofi -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140808/5fe1dd9e/attachment.html>