--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on June 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] multiple switch on one variable



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>