--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on December 2012 ---
Hello, Is there a way to use Frama on programs which contain pointers to functions and the invocation of those functions using the (*myfunc)() notation? I see that equality comparison is available for function pointers in the ACSL. I have attempted to implement a preprocessor which converts the following code into something Frama seems to want. void func1() { ... } void func2() { ... } int main() { void (*myFunc)(); myFunc = &func1; (*myFunc)(); myFunc = &func2; (*myFunc)(); } my preprocessor then created: int main() { void (*myFunc)(); myFunc = &func1; (*myFunc)(); if (myFunc == &func1) { func1();} else if (myFunc == &func2) { func2();} else { printf("unhappiness\n"); exit(0); } myFunc = &func2; if (myFunc == &func1) { func1();} else if (myFunc == &func2) { func2();} else { printf("unhappiness\n"); exit(0); } } My preprocessor has become progressively far more complex than needed in order to handle return values and function arguments. It just seems there might be an easier way.... Your thoughts? Sincerely, Daniel Chapiesky