Decouple pointer-check and pointer-arithmetic overflow

In 0779bbd additional checks for arithmetic overflow on pointer
arithmetic were added, and enabled implicitly when --pointer-check was
set. This is now decoupled and a new option --pointer-overflow-check is
available.

Author: tautschnig

src/analyses/goto_check.cpp

@@ -40,6 +40,7 @@ class goto_checkt
     enable_div_by_zero_check=_options.get_bool_option("div-by-zero-check");
     enable_signed_overflow_check=_options.get_bool_option("signed-overflow-check");
     enable_unsigned_overflow_check=_options.get_bool_option("unsigned-overflow-check");
+    enable_pointer_overflow_check=_options.get_bool_option("pointer-overflow-check");
     enable_undefined_shift_check=_options.get_bool_option("undefined-shift-check");
     enable_float_overflow_check=_options.get_bool_option("float-overflow-check");
     enable_simplify=_options.get_bool_option("simplify");
@@ -103,6 +104,7 @@ class goto_checkt
   bool enable_div_by_zero_check;
   bool enable_signed_overflow_check;
   bool enable_unsigned_overflow_check;
+  bool enable_pointer_overflow_check;
   bool enable_undefined_shift_check;
   bool enable_float_overflow_check;
   bool enable_simplify;
@@ -899,7 +901,7 @@ void goto_checkt::pointer_overflow_check(
   const exprt &expr,
   const guardt &guard)
 {
-  if(!enable_pointer_check)
+  if(!enable_pointer_overflow_check)
     return;
 
   if(expr.id()==ID_plus ||

src/analyses/goto_check.h

@@ -32,7 +32,7 @@ void goto_check(
 #define GOTO_CHECK_OPTIONS \
   "(bounds-check)(pointer-check)(memory-leak-check)" \
   "(div-by-zero-check)(signed-overflow-check)(unsigned-overflow-check)" \
-  "(undefined-shift-check)" \
+  "(pointer-overflow-check)(undefined-shift-check)" \
   "(float-overflow-check)(nan-check)"
 
 #define GOTO_CHECK_HELP \
@@ -42,6 +42,7 @@ void goto_check(
   " --div-by-zero-check          enable division by zero checks\n" \
   " --signed-overflow-check      enable signed arithmetic over- and underflow checks\n" \
   " --unsigned-overflow-check    enable arithmetic over- and underflow checks\n" \
+  " --pointer-overflow-check     enable pointer arithmetic over- and underflow checks\n" \
   " --undefined-shift-check      check shift greater than bit-width\n" \
   " --float-overflow-check       check floating-point for +/-Inf\n" \
   " --nan-check                  check floating-point for NaN\n" \
@@ -53,6 +54,7 @@ void goto_check(
   options.set_option("div-by-zero-check", cmdline.isset("div-by-zero-check")); \
   options.set_option("signed-overflow-check", cmdline.isset("signed-overflow-check")); \
   options.set_option("unsigned-overflow-check", cmdline.isset("unsigned-overflow-check")); \
+  options.set_option("pointer-overflow-check", cmdline.isset("pointer-overflow-check")); \
   options.set_option("undefined-shift-check", cmdline.isset("undefined-shift-check")); \
   options.set_option("float-overflow-check", cmdline.isset("float-overflow-check")); \
   options.set_option("nan-check", cmdline.isset("nan-check"))