--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on June 2011 ---
Hello, I need some help.. Actually, if we have two "switch" on the same variable, frama-c doesn't seem to understand that it is really the same variable. Let me explain what I mean: Suppose that you have the following code: /*@ ensures \result == x || \result == a + b; */ int main (int a, int b, int x) { int y; switch (x) { case 1 : a = 5; break; case 2: b = 3 ; break; } y = a + b; switch (x) { case 3: b= 1; break; case 4: a = 0; break; } if (a =5) return x; return y; } Remark that x is not modified during the function. In that case, frama-c/ Jessie will check the postcondition for the cases that (x=1 and x=3) as well as (x=1 and x=4) and go on.. Unless that normally we will never have both x= 1 and x= 3 at the same time. Does anyone have any idea about how to explain that to frama-c? Thanks in advance! Maria PS: I am using Beryllium-20090902. So if it is not the cas for a later version, please let me know. -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110617/e694300c/attachment.htm>