From 591d8829e10ee86dde7e9a0de460828687c6b979 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <mt@debian.org>
Date: Wed, 12 Apr 2017 08:45:02 +0100
Subject: [PATCH] Do not treat integer literals 0u, 0l as base-8

Only literals with a digit following the initial 0 should be understood as
base-8.
---
 regression/cbmc/unsigned1/main.c                | 6 ++++++
 regression/cbmc/unsigned1/test.desc             | 8 ++++++++
 src/ansi-c/literals/convert_integer_literal.cpp | 2 +-
 3 files changed, 15 insertions(+), 1 deletion(-)
 create mode 100644 regression/cbmc/unsigned1/main.c
 create mode 100644 regression/cbmc/unsigned1/test.desc

diff --git a/regression/cbmc/unsigned1/main.c b/regression/cbmc/unsigned1/main.c
new file mode 100644
index 00000000000..39a31810c57
--- /dev/null
+++ b/regression/cbmc/unsigned1/main.c
@@ -0,0 +1,6 @@
+int main()
+{
+  unsigned x;
+  x=0u;
+  return 0;
+}
diff --git a/regression/cbmc/unsigned1/test.desc b/regression/cbmc/unsigned1/test.desc
new file mode 100644
index 00000000000..a1e381cbf60
--- /dev/null
+++ b/regression/cbmc/unsigned1/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--show-goto-functions
+^EXIT=0$
+^SIGNAL=0$
+--
+00u
+^warning: ignoring
diff --git a/src/ansi-c/literals/convert_integer_literal.cpp b/src/ansi-c/literals/convert_integer_literal.cpp
index 3412f02bd2c..d7c832dee31 100644
--- a/src/ansi-c/literals/convert_integer_literal.cpp
+++ b/src/ansi-c/literals/convert_integer_literal.cpp
@@ -75,7 +75,7 @@ exprt convert_integer_literal(const std::string &src)
     std::string without_prefix(src, 2, std::string::npos);
     value=string2integer(without_prefix, 2);
   }
-  else if(src.size()>=2 && src[0]=='0')
+  else if(src.size()>=2 && src[0]=='0' && isdigit(src[1]))
   {
     // octal
     base=8;