While the observe semantics example is somewhat scary, it isn't the end of the world. It is more than likely that `foo` dereferences p in the function body anyway, so the UB in the precondition is inconsequential.