--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on May 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Uncaught exception



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