Pointer arithmetic has two operands by construction

Simplify the code accordingly and include a regression test that exercises it.

Author: tautschnig

regression/cbmc/pointer-overflow1/main.c

@@ -0,0 +1,17 @@
+#include <stdlib.h>
+
+int main() {
+  int *p = malloc(2 * sizeof(int)), *p2;
+  size_t other1, other2;
+
+  p2 = p + other1;
+  p2 = p + other2 + other1;
+  p2 = other1 + other2 + p;
+  p2 = p - other1;
+  p2 = p - other2 - other1;
+
+  p2 = p + sizeof(int);
+  p2 = p + sizeof(int) + sizeof(int);
+
+  return 0;
+}

regression/cbmc/pointer-overflow1/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--pointer-overflow-check --unsigned-overflow-check
+^EXIT=10$
+^SIGNAL=0$
+^\[main\.overflow\.\d+\] (pointer )?arithmetic overflow on .*sizeof\(signed int\) .* : SUCCESS
+^VERIFICATION FAILED$
+^\*\* 8 of 11 failed
+--
+^\[main\.overflow\.\d+\] (pointer )?arithmetic overflow on .*sizeof\(signed int\) .* : FAILURE
+^warning: ignoring

src/analyses/goto_check.cpp

@@ -894,23 +894,22 @@ void goto_checkt::pointer_overflow_check(
   if(!enable_pointer_overflow_check)
     return;
 
-  if(expr.id()==ID_plus ||
-     expr.id()==ID_minus)
-  {
-    if(expr.operands().size()==2)
-    {
-      exprt overflow("overflow-"+expr.id_string(), bool_typet());
-      overflow.operands()=expr.operands();
+  if(expr.id() != ID_plus && expr.id() != ID_minus)
+    return;
 
-      add_guarded_claim(
-        not_exprt(overflow),
-        "pointer arithmetic overflow on "+expr.id_string(),
-        "overflow",
-        expr.find_source_location(),
-        expr,
-        guard);
-    }
-  }
+  if(expr.operands().size() != 2)
+    throw "pointer arithmetic expected to have exactly 2 operands";
+
+  exprt overflow("overflow-" + expr.id_string(), bool_typet());
+  overflow.operands() = expr.operands();
+
+  add_guarded_claim(
+    not_exprt(overflow),
+    "pointer arithmetic overflow on " + expr.id_string(),
+    "overflow",
+    expr.find_source_location(),
+    expr,
+    guard);
 }
 
 void goto_checkt::pointer_validity_check(
@@ -1436,11 +1435,7 @@ void goto_checkt::check_rec(
     if(expr.type().id()==ID_signedbv ||
        expr.type().id()==ID_unsignedbv)
     {
-      if(expr.operands().size()==2 &&
-         expr.op0().type().id()==ID_pointer)
-        pointer_overflow_check(expr, guard);
-      else
-        integer_overflow_check(expr, guard);
+      integer_overflow_check(expr, guard);
     }
     else if(expr.type().id()==ID_floatbv)
     {