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] 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