--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on December 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Following execution through function pointer



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