--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on May 2010 ---
I am leaving some of your questions for the experts who also read this list. > One thing I noticed when experimenting with definition and declaration > annotations is that "assign \nothing;" does not mean "no side > effects". No, please backtrack to this point in your reasoning. "assigns \nothing ;" does mean "no side effects". Example: t.c: static x; /*@ assigns x ; */ void f(void) { x = 12; } ___ t.h: /*@ assigns \nothing ; */ void f(void); ___ frama-c t.c t.h [kernel] preprocessing with "gcc -C -E -I. t.c" [kernel] preprocessing with "gcc -C -E -I. t.h" t.c:5:[kernel] warning: found contradictory assign clauses. Keeping only one Either you did not pay attention to this warning, or you typed "frama-c t.c". You do not have to list header files that are included in at least one .c file in your project, but you have to be aware that frama-c 1) uses standard pre-processing, and 2) only looks at files you list (modulo clause 1). Pascal