--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on February 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Strange results



Hello,

Can someone help me to understand those results ?

On this kind of code :

int x3;
if (p->a) { x3 = in; }
else { x3 = p->b; }

with the following computed values :

in ? [--..--]
p ? {‌{ &T + [242..1959] }‌}
p->a ? [--..--] or UNINITIALIZED
p->b ? [--..--] or UNINITIALIZED

The else branch is marked as dead (highlighted in red in the GUI).
I don't understand why the branch is dead, and moreover,
I don't understand why there is no generated assert...
I don't see any messages about that in the log.

I didn't manage to reproduce on a small example since in all my tests
I always get   assert \initialized(&p->a)   as expected.

I don't know if it is important, but the fields a and b are unsigned char.
Hope there is enough information for you to understand what this is about.

Thank you in advance for your help.
-- 
Anne.