add a check for overflow on unsigned unary minus

This adds a check that the operand of an unsigned unary minus is not zero
when unsigned overflow checks are enabled.

Closes #6114.

Author: kroening

regression/cbmc/overflow/unary_minus_overflow.c

@@ -0,0 +1,22 @@
+#include <limits.h>
+
+int main()
+{
+  signed int x, y;
+
+  x = INT_MIN;
+
+  // this is an overflow
+  y = -x;
+
+  // ok
+  x = -(x + 1);
+
+  unsigned a, b;
+
+  a = 1;
+  a = -a; // overflow, -1 is not representable
+
+  b = 0;
+  b = -b; // ok
+}

regression/cbmc/overflow/unary_minus_overflow.desc

@@ -0,0 +1,10 @@
+CORE
+unary_minus_overflow.c
+--signed-overflow-check --unsigned-overflow-check
+^EXIT=10$
+^SIGNAL=0$
+^\[.*\] line .* arithmetic overflow on signed unary minus in -x: FAILURE$
+^\[.*\] line .* arithmetic overflow on signed unary minus in -\(x \+ 1\): SUCCESS$
+^\[.*\] line .* arithmetic overflow on unsigned unary minus in -a: SUCCESS$
+^\[.*\] line .* arithmetic overflow on unsigned unary minus in -b: FAILURE$
+--

src/analyses/goto_check.cpp

@@ -734,8 +734,8 @@ void goto_checkt::integer_overflow_check(
   {
     if(type.id()==ID_signedbv)
     {
-      // overflow on unary- can only happen with the smallest
-      // representable number 100....0
+      // overflow on unary- on signed integers can only happen with the
+      // smallest representable number 100....0
 
       equal_exprt int_min_eq(
         to_unary_minus_expr(expr).op(), to_signedbv_type(type).smallest_expr());
@@ -748,6 +748,22 @@ void goto_checkt::integer_overflow_check(
         expr,
         guard);
     }
+    else if(type.id() == ID_unsignedbv)
+    {
+      // Overflow on unary- on unsigned integers happens for all operands
+      // that are not zero.
+
+      notequal_exprt not_eq_zero(
+        to_unary_minus_expr(expr).op(), to_unsignedbv_type(type).zero_expr());
+
+      add_guarded_property(
+        not_eq_zero,
+        "arithmetic overflow on unsigned unary minus",
+        "overflow",
+        expr.find_source_location(),
+        expr,
+        guard);
+    }
 
     return;
   }