Pascal, thanks for the update about flags!
Dara, I forgot if you said you'd tried it already, but it's possible
that kcc can check for the strict aliasing issues:
https://code.google.com/p/c-semantics/
Strict aliasing is surely one of the nastiest things the C standard
committee ever did to programmers.
John
On 6/2/13 10:51 AM, Pascal Cuoq wrote:
Hello, all.
1) Signed overflow
for(char c = 1; c; c++) ;
Many people -- including, I'm guessing, the Frama-C authors -- do
not believe that this construct leads to undefined overflows. Some
discussion of the issues can be found here:
http://blog.regehr.org/__archives/482
<http://blog.regehr.org/archives/482>
As John says. “c++” is represented internally as “c = (char)((int)c +
1)”. You can obtain a print-out of the internal AST in compilable C form
with “frama-c -print”. I mostly use it as a crutch when I have a doubt
about precedence of operators in C, and for this example, it shows:
char c;
c = (char)1;
while (c) c = (char)((int)c + 1);
The C99 clause on which we base our reasoning is 6.3.1.1:2
<http://6.3.1.1:2>.
2) Invalid union accesses
union { char c; short s; } u;
u.s = 1;
u.c = 0;
printf("%d\n", u.s);
This is considered implementation-defined in Frama-C and I went to
considerable trouble to make sure the value analysis precisely predicted
the result of this sequence of operations. It is not much of a stretch
to consider that this use of unions is covered by footnote 82 in C99TC3.
3) Aliased access to unions
union { char c; short s; } u;
char *c = &u.c;
short *s = &u.s;
*c = 1;
*s = 2;
printf("%d\n", u.s);
It was my great disappointment while working on Csmith-related matter to
find out that C99's 6.5:7 clause could be interpreted as meaning that
the above was undefined. In any case, Frama-C's value analysis manual
notes that the status of “strict aliasing verification” is that it is a
feature that it is possible to request.
Also, I've been using the frama-c from
creduce/scripts/test1_wrong___code_framac.sh and two of the
options don't seem to exist on the latest (Fluorine) release:
-val-signed-overflow-alarms and -precise-unions . If anybody
knows their current equivalents, that would be most helpful!
Option “-precise-unions” in older Frama-C versions activates the code
that gave me so much work to make sure example 2) was interpreted
precisely. It was guarded by a command-line option because there could
be a performance penalty. Now that Frama-C's value analysis was
restructured, there no longer is any penalty. This option no longer
exists, and the analyzer behaves as if the option was always on.
Option “-val-signed-overflow-alarms” underwent two changes: it
became -warn-signed-overflow, and it became on by default. So again, no
option is necessary in Fluorine to emulate the previous behavior.
I don't think any of us have yet upgraded to Fluorine, perhaps
Pascal can comment on the best current flags to use to make Frama-C
into a checking interpreter.
These two options should be the only options to remove from the script
when using Fluorine. I have done a little bit of Csmith-testing before
the release, but I may have forgotten what else I had to change, so do
not hesitate to ask if something seems askew.
Pascal
