--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on April 2011 ---
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])(); }