function pointer

[Nguyễn Thu Trang]

Hi, 

I used CBMC to check for assertions in a function in which a parameter is a function pointer.  It can't verify or generate counterexamples for my assertions. It said that assignment to 'symbol ' not handled. In addition, it also said that replacing function pointer by 1 possible targets. 

Could you please show me how to verify my assertions in this case?

Thank you very much.

Trang.

[Martin Nyx Brain]

CBMC handles function pointers by scanning the program for all
functions that could possibly be passed as a function pointer and then
transforming the code to call each possibility. It can't handle truly
"open" programs. You will need to create a "harness" that calls the
function you want to verify with a number of alternatives for the
function pointers.

HTH

Cheers,
- Martin