--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on February 2013 ---
Le 08/02/2013 12:07, Boris Yakobowski a ?crit : > 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 ? Bravo Boris ! p->a is always 1, so the else branch is dead ! So it means that I mustn't trust to much the GUI... to bad :-( Thank you VERY much. -- Anne.