--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on April 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] problem with pre-processing



On Mon, Apr 11, 2011 at 3:24 PM, SENE, Sali <sali.sene at airbus.com> wrote:
> Thank you Pascal it solve the problem.
> I have another question: does Frama-c support pointer on function?

The framework handles function pointers. Then, for this kind of difficult
construct, it is up to each plug-in to decide and document whether it
is supported in that plug-in or not. Function pointers are supported
in the value analysis plug-in, which can analyse the example below
and tell with the command-line

frama-c -val -main f t.c

that h1() and h3() are called.

Pascal

typedef void (*T_FUN)();
extern void h0(), h1(), h2(), h3(), h4();
const T_FUN t[]={h0,h1,h2,h3,h4};
int g;
volatile int v;
void f(int a, int *b, int *c, int *d) {
    int i=*d;
    *b=i;
    if (*b) *b=g;
    else *c=g+a;
    v=*b;
    while (v && i>314) i/=3;
    for (i=0; i<5; i++) if (*c && i%2) (*t[i])();
}