--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on February 2013 ---
Hi, On Fri, Feb 8, 2013 at 11:52 AM, Anne Pacalet <anne.pacalet at free.fr> wrote: > if (p->a) { x3 = in; } > else { x3 = p->b; } > [snip] > p ? {{ &T + [242..1959] }} > p->a ? [--..--] 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. This might be a consequence of the way the GUI displays the values of lval accessed through an imprecise pointer. Can you re-run the analysis with the following instrumentation ? Frama_C_show_each(p, p->a); if (p->a) { x3 = in; } else { x3 = p->b; } and report your results ? -- Boris