thanks to your suggestion of Frama-C, I've had a lot more luck with reducing
wrong code bugs. I have noticed a few sorts of errors that Frama-C doesn't
seem to flag though. I was curious if other people have encountered these, and
what, if any workarounds can be used:
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
2) Invalid union accesses
union { char c; short s; } u;
u.s = 1;
u.c = 0;
printf("%d\n", u.s);
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);
Perhaps Pascal can comment on these.
#2 is not exactly invalid, but rather is unspecified (unless there's
something undefined going on with padding). However, GCC provides good
guarantees about this case, even if other compilers might not. It could
be that the Frama-C people have sided with GCC.
#3 looks undefined.
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!
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.
John
