--- layout: fc_discuss_archives title: Message 41 from Frama-C-discuss on January 2011 ---
On Thu, Jan 20, 2011 at 4:40 PM, David MENTRE <dmentre at linux-france.org> wrote: > 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++;"? The first i++ is the loop incrementation, while the second one is your i = i+1. Cil (which is used by Frama-C as parser) does not record the difference between i=i+1, i+=1 and i++, and chooses to print them using the most idiomatic form. In debug mode, the printer is as simple as possible, and print incrementation using += . > ?* 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? Depending on how I read your question, the answer may be yes or no. If by "after the while loop()" you reason syntactically and mean just above the "return" statement, then the answer is no. A this point, i only has value 10, as can be seen by evaluating it with the right-button menu. "Next statement" (both the printed message and the notion used by Cil) actually refer to the execution flow of the program. In this case, the control flows from i++ to the while itself (sid 2), and we once more have 0 in the possible values for i (in case we haven't started iterating). -- Boris