From d7388838ce8ab55e915049d1efd14c84cc2671f6 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Sat, 5 Jan 2019 16:12:43 +0000
Subject: [PATCH 1/2] bugfix: use -std=gnu89 for C

This fixes a copy & paste error.
---
 src/ansi-c/c_preprocess.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/ansi-c/c_preprocess.cpp b/src/ansi-c/c_preprocess.cpp
index 16f0752643b..bfd58b502a5 100644
--- a/src/ansi-c/c_preprocess.cpp
+++ b/src/ansi-c/c_preprocess.cpp
@@ -610,7 +610,7 @@ bool c_preprocess_gcc_clang(
     switch(config.ansi_c.c_standard)
     {
     case configt::ansi_ct::c_standardt::C89:
-      argv.push_back("-std=gnu++89");
+      argv.push_back("-std=gnu89");
       break;
 
     case configt::ansi_ct::c_standardt::C99:

From ae786094137e40c6c23988f30e87290f30702fee Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Sat, 5 Jan 2019 11:54:53 +0000
Subject: [PATCH 2/2] signed left-shift overflow depends on standard version

The semantics of signed left shifts are contentious for the case
that a '1' is shifted into the signed bit.
Assuming 32-bit integers, 1<<31 is implementation-defined
in ANSI C and C++98, but is explicitly undefined by C99,
C11 and C++11.
---
 regression/cbmc/Overflow_Leftshift1/main.c    |  5 ++-
 .../{test.desc => test-c89.desc}              |  3 +-
 src/analyses/goto_check.cpp                   | 35 +++++++++++++++++--
 3 files changed, 38 insertions(+), 5 deletions(-)
 rename regression/cbmc/Overflow_Leftshift1/{test.desc => test-c89.desc} (84%)

diff --git a/regression/cbmc/Overflow_Leftshift1/main.c b/regression/cbmc/Overflow_Leftshift1/main.c
index cdc26ac2ef3..7d52799f096 100644
--- a/regression/cbmc/Overflow_Leftshift1/main.c
+++ b/regression/cbmc/Overflow_Leftshift1/main.c
@@ -3,7 +3,7 @@ int main()
   unsigned char x;
 
   // signed, owing to promotion, and may overflow
-  unsigned r=x << ((sizeof(unsigned)-1)*8);
+  unsigned r = x << ((sizeof(unsigned) - 1) * 8 + 1);
 
   // signed, owing to promotion, and cannot overflow
   r=x << ((sizeof(unsigned)-1)*8-1);
@@ -20,5 +20,8 @@ int main()
   // distance too far, not an overflow
   s = s << 100;
 
+  // not an overflow in ANSI-C, but undefined in C99
+  s = 1 << (sizeof(int) * 8 - 1);
+
   return 0;
 }
diff --git a/regression/cbmc/Overflow_Leftshift1/test.desc b/regression/cbmc/Overflow_Leftshift1/test-c89.desc
similarity index 84%
rename from regression/cbmc/Overflow_Leftshift1/test.desc
rename to regression/cbmc/Overflow_Leftshift1/test-c89.desc
index c7b2f8119c0..88d83ff7a86 100644
--- a/regression/cbmc/Overflow_Leftshift1/test.desc
+++ b/regression/cbmc/Overflow_Leftshift1/test-c89.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---signed-overflow-check
+--signed-overflow-check --c89
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*\] line 6 arithmetic overflow on signed shl in .*: FAILURE$
@@ -13,3 +13,4 @@ main.c
 ^warning: ignoring
 ^\[.*\] line 12 arithmetic overflow on signed shl in .*: .*
 ^\[.*\] line 21 arithmetic overflow on signed shl in .*: .*
+^\[.*\] line 24 arithmetic overflow on signed shl in .*: .*
diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index 8bb91835390..b66ba43c6e6 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/array_name.h>
 #include <util/base_type.h>
 #include <util/c_types.h>
+#include <util/config.h>
 #include <util/cprover_prefix.h>
 #include <util/expr_util.h>
 #include <util/find_symbols.h>
@@ -662,12 +663,40 @@ void goto_checkt::integer_overflow_check(
 
       const exprt op_ext_shifted = shl_exprt(op_ext, distance);
 
-      // get top bits of the shifted operand
+      // The semantics of signed left shifts are contentious for the case
+      // that a '1' is shifted into the signed bit.
+      // Assuming 32-bit integers, 1<<31 is implementation-defined
+      // in ANSI C and C++98, but is explicitly undefined by C99,
+      // C11 and C++11.
+      bool allow_shift_into_sign_bit = true;
+
+      if(mode == ID_C)
+      {
+        if(
+          config.ansi_c.c_standard == configt::ansi_ct::c_standardt::C99 ||
+          config.ansi_c.c_standard == configt::ansi_ct::c_standardt::C11)
+        {
+          allow_shift_into_sign_bit = false;
+        }
+      }
+      else if(mode == ID_cpp)
+      {
+        if(
+          config.cpp.cpp_standard == configt::cppt::cpp_standardt::CPP11 ||
+          config.cpp.cpp_standard == configt::cppt::cpp_standardt::CPP14)
+        {
+          allow_shift_into_sign_bit = false;
+        }
+      }
+
+      const unsigned number_of_top_bits =
+        allow_shift_into_sign_bit ? op_width : op_width + 1;
+
       const exprt top_bits = extractbits_exprt(
         op_ext_shifted,
         new_type.get_width() - 1,
-        op_width - 1,
-        unsignedbv_typet(op_width + 1));
+        new_type.get_width() - number_of_top_bits,
+        unsignedbv_typet(number_of_top_bits));
 
       const exprt top_bits_zero =
         equal_exprt(top_bits, from_integer(0, top_bits.type()));