--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on February 2013 ---
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.