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

[Frama-c-discuss] Strange results



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