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

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