function pointer

8 views
Skip to first unread message

Nguyễn Thu Trang

unread,
Jul 6, 2019, 9:15:59 AM7/6/19
to CProver Support
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

unread,
Jul 8, 2019, 12:33:36 PM7/8/19
to cprover...@googlegroups.com
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

Reply all
Reply to author
Forward
0 new messages