Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Strange results

  • Subject: [Frama-c-discuss] Strange results
  • From: anne.pacalet at free.fr (Anne Pacalet)
  • Date: Fri, 08 Feb 2013 11:52:39 +0100
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.