--- layout: fc_discuss_archives title: Message 38 from Frama-C-discuss on March 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] precision for expression evaluation in acondition



> 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