Permit re-declaring anonymous enum types

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@5334 6afb6bc1-c8e4-404c-8f48-9ae832c5b171

regression/ansi-c/enum5/main.c

@@ -0,0 +1,30 @@
+static void foo()
+{
+  enum {
+    COL_CUR,
+    COL_CHG,
+    COL_AVG,
+    COL_MA10,
+    COL_MA100,
+    COL_MA1000,
+    COL_LAST
+  } col;
+}
+
+static void bar()
+{
+  enum {
+    COL_CUR,
+    COL_CHG,
+    COL_AVG,
+    COL_MA10,
+    COL_MA100,
+    COL_MA1000,
+    COL_LAST
+  } col;
+}
+
+int main()
+{
+  return 0;
+}

regression/ansi-c/enum5/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$

src/ansi-c/c_typecheck_type.cpp

@@ -1151,8 +1151,14 @@ void c_typecheck_baset::typecheck_c_enum_type(typet &type)
     }
     else if(symbol.type.id()==ID_c_enum)
     {
-      err_location(type);
-      throw "redeclaration of enum tag";
+      // We might already have the same anonymous enum, and this is
+      // simply ok. Note that the C standard treats these as
+      // different types.
+      if(!base_name.empty())
+      {
+        err_location(type);
+        throw "redeclaration of enum tag";
+      }
     }
     else
     {