--- layout: fc_discuss_archives title: Message 74 from Frama-C-discuss on April 2009 ---
[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