Lennart Beringer

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) {...

…s, to facilitate proof of lemma func_at_valid_pointer and ensuing lemmas about func_ptr and func_ptr'