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