[SwayamInSync]

C++17 [expr.add]/5 defines the difference of two null pointers as 0, but the verifier required both operands of every pointer difference to be non-null. Any contract that allows an empty range then failed:

long same_empty(const int *a, int n)
  cppverify::pre(cppverify::valid(a, n) && n == 0)
  cppverify::post(cppverify::result == 0)
{
  const int *b = a;
  return b - a;
}

On main this fails pointer-difference with a = 0, b = 0, and so does the usual q - a after a loop that walks q from a when n == 0 is allowed.

The checks of a pointer difference (non-null operands, one origin, positions in the object) now hold when both operands are null. The value is already 0, since null is address 0. A null pointer minus a non-null one, or the reverse, still fails. pointer_difference_fail.cpp expected nullptr - nullptr to fail, the rule this corrects; that case is now both_null in the new test.

Testing: suite/pointer_difference_null.cpp fails on main (same_empty, both_null, walked), and accepting either operand null instead of both lets null_minus_object verify and one_null go unresolved. Verify suite: 398 passed, 1 unsupported. A verdict differential against main over the 405 Verify sources changes only nullptr - nullptr in pointer_difference_fail.cpp; decode_uleb128_length_11 (llvm_uleb128_decoder_exhaustive.cpp) timed out on main under load in that run and verified in every other run of either binary.