Eliminate postcondition_allows_exit / correct NullExtension.Espec

[lennartberinger]

Lemma semax_prog_rule (in veric/semax_prog) contains the assumption
"postcondition_allows_exit tint" which is actually False for the current definition of NullExtension, rendering the lemma true but inapplicable. If postcondition_allows_exit must be retained, a possible solution may be to change the definition of NullExtenion's ext_spec_exit component from False to True.