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