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] Value analysis emits warning for for-loop

>  for(i=0; i<10; i++) ;
>- why does it warn about the assignment i=0?
>tst8.c:4: Warning: assigning non deterministic value for the first time

I forgot to mention that the warning was not about the assignment
"i=0;" which is always deterministic, but about the other
assignment on line 4, "i++", which appears like it could
be the first assignment to introduce non-determinism in the
analysis.

In fact this assignment is not responsible, the non-determinism
is introduced an instant earlier when several iterations of the loop
are joined together by the analyzer (but you have a message for
that too).

Although here, this warning is noise, I could show you examples
where it is useful. While I think of it, these examples should probably
be in the documentation, but not in the section I quoted earlier.
The should be in a different section dedicated to the use of the value analysis
for the symbolic execution of deterministic programs. The problem is that
there are so many different ways to use the value analysis that
it's taking a long time to document all of them, but we're slowly getting
there.

Pascal