I do it today; your assumption that "it would" is incorrect.
void z(value* x) {
/* preconditions. */
MODEL_ASSERT(valid_value_ptr(x));
/* do operation. */
/* postconditions. */
MODEL_ASSERT(z_postcondition(a, b));
}
In practice:
z(NULL); /* model failure. */
z(&uninitialized_value_on_stack); /* model failure. */
It works, and the model checker runs in seconds.
