--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on December 2012 ---
> If you intend to use a plugin that do not support function > pointers, I'd suggest that you take advantage of the information > computed by Value Analysis in order to generate the possible cases, > instead of an external pre-processor. In the easiest case, where each > function pointer points to a unique function, you just have to call the > semantic constant folding plug-in to get rid of them. This looks like this. Original: int printf(const char *f, ...); void func1(void) { printf("boo!"); } void func2(void) { printf("bah"); } int main() { void (*myFunc)(); myFunc = &func1; 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); } } $ frama-c -scf t.c /* Generated by Frama-C */ /*@ assigns \at(\result,Post) \from *f; */ extern int printf(char const *f , ...); void func1(void) { printf("boo!"); return; } void func2(void) { printf("bah"); return; } extern int ( /* missing proto */ exit)(int x_0); int main(void) { int __retres; void (*myFunc)(); myFunc = (void (*)())(& func1); if (1) { func1(); } else { if (myFunc == & func2) { func2(); } else { printf("unhappiness\n"); exit(0); } } myFunc = (void (*)())(& func2); if (0) { func1(); } else { if (1) { func2(); } else { printf("unhappiness\n"); exit(0); } } __retres = 0; return (__retres); } The value of variable myFunc has not been replaced inside the if conditions that were unreachable. Hopefully that won't be an issue.