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