Given a function pointer f specified by func_ptr or func_ptr', it does not appear
possible to write a C program that tests f against NULL, as in "if (f) { foo } else { bar}":
the spatial clause of func_ptr' is emp while verifying the comparison needs
"valid_pointer f" (to establish denote_tc_test_eq f nullval").
CompCert 3.13 correctly sets the permission of the function's address to Nonempty
in line 654 of https://github.com/AbsInt/CompCert/blob/3.13/common/Globalenvs.v,
so this is likely a shortcoming of VST's construction of the resources associated with this address.
Given a function pointer f specified by func_ptr or func_ptr', it does not appear possible to write a C program that tests f against NULL, as in "if (f) { foo } else { bar}": the spatial clause of func_ptr' is emp while verifying the comparison needs "valid_pointer f" (to establish denote_tc_test_eq f nullval"). CompCert 3.13 correctly sets the permission of the function's address to Nonempty in line 654 of https://github.com/AbsInt/CompCert/blob/3.13/common/Globalenvs.v, so this is likely a shortcoming of VST's construction of the resources associated with this address.