--- layout: fc_discuss_archives title: Message 38 from Frama-C-discuss on March 2011 ---
> I don't know the value analysis very well but maybe it is related > to the fact that you do not provide an initial value for toto. > If I modify your programm like > > ? int toto; > ? printf("%d\n", toto); > > then I get the value > > 1606415944 Considering that it's the value of variable bar the discussion is about, and that the program is safe from uninitialized access (until you modify it with your call to printf), I do not think that this is related. You can learn about the value analysis by typing "frama-c -val test.c" on Xavier's example. It will tell you that the original uses toto correctly and that your modification accesses toto unsoundly. Uninitialized variables passed as arguments to library functions is a vexing problem for technical reasons that would take too long to describe here, but if you are using patchlevel 1 of Carbon's value analysis, you will get: t.c:5:[kernel] warning: accessing uninitialized left-value toto: assert(Ook) Link: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2011-February/002527.html It's one of the fixes for 2011/02/12. It may have been working correctly in previous versions. As I said, it is a vexing issue. Pascal