Frama-C-discuss mailing list archives
This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Frama-c-discuss] Following execution through function pointer
- Subject: [Frama-c-discuss] Following execution through function pointer
- From: dchapiesky2 at gmail.com (daniel)
- Date: Thu, 13 Dec 2012 22:33:06 -0500
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
- Follow-Ups:
- [Frama-c-discuss] Following execution through function pointer
- From: virgile.prevosto at m4x.org (Virgile Prevosto)
- [Frama-c-discuss] Following execution through function pointer
- Prev by Date: [Frama-c-discuss] Help to write the specification in ACSL
- Next by Date: [Frama-c-discuss] Following execution through function pointer
- Previous by thread: [Frama-c-discuss] Help to write the specification in ACSL
- Next by thread: [Frama-c-discuss] Following execution through function pointer
- Index(es):