Try using the RMC vtable cache to restrict CBMC function pointers via this intertface: http://cprover.diffblue.com/md__home_travis_build_diffblue_cbmc_doc_architectural_restrict-function-pointer.html