Not all potential null dereferences are covered by the verifier, they even give an example where the rule is not triggered, but null may be dereferenced by the code.
Now that's a bug. If it can't be ruled out at compile time, there should have to be a check at run time.