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] Issue on value analysis with loops

Hello Boris,

2011/1/20 Boris Yakobowski <boris at yakobowski.org>:
> Yes, almost: it is actually the "while" itself, not the join point
> after it. What is called "Next statement" in the context of "i=0" is
> actually a "while(1)" statement, which is transparently printed as
> "while(i<10)" by Frama-C. On this while statement, i takes the values
> 0,2,4,6,8,10, as the value 10 is pruned out only later, in an "if"
> inside the while. You can see that yourself by invoking frama-c with
> the option -kernel-debug 1

Thanks a lot, the -kernel-debug 1 option helps!

Two other questions for the same program:
 * Why the "i = i + 1" in the for() loop of the original program is
transformed into "i++; i++;"?

 * Why value 0 appears for next statement's value of the last "i++" in
the loop (sid: 7 in the debug version)? I would have expected "i ? {2;
4; 6; 8; 10; }". Is it because, once again, the next statement is the
point after the while() loop?

Best regards,
d.