--- layout: fc_discuss_archives title: Message 40 from Frama-C-discuss on January 2011 ---
[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.