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