C front-end: refuse duplicate declaration of local variable

regression/ansi-c/duplicate_local1/main.c

@@ -0,0 +1,15 @@
+// duplicate globals are accepted by compilers
+int x;
+int x;
+
+int main()
+{
+  int a = 10;
+
+  // gcc: error: redeclaration of 'a' with no linkage
+  int a;
+
+  a++;
+
+  return 0;
+}

regression/ansi-c/duplicate_local1/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+
+redeclaration of 'main::1::a' with no linkage$
+CONVERSION ERROR
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+redeclaration of 'x' with no linkage$

regression/cbmc-shadow-memory/nondet-size-arrays1/main.c

@@ -69,12 +69,12 @@ int main()
   assert(__CPROVER_get_field(z + 4, "field1") == 15);
   assert(__CPROVER_get_field(z + 4, "field2") == 16);
 
-  int i;
-  __CPROVER_assume(0 <= i && i < n);
-  __CPROVER_set_field(&(B[i]), "field1", 42);
-  assert(__CPROVER_get_field(&(B[i]), "field1") == 42);
+  int j;
+  __CPROVER_assume(0 <= j && j < n);
+  __CPROVER_set_field(&(B[j]), "field1", 42);
+  assert(__CPROVER_get_field(&(B[j]), "field1") == 42);
 
-  z = &(B[i]);
+  z = &(B[j]);
   __CPROVER_set_field(z, "field1", 43);
   assert(__CPROVER_get_field(z, "field1") == 43);
 
@@ -101,12 +101,12 @@ int main()
   assert(__CPROVER_get_field(z + 4, "field1") == 15);
   assert(__CPROVER_get_field(z + 4, "field2") == 16);
 
-  int i;
-  __CPROVER_assume(0 <= i && i < n);
-  __CPROVER_set_field(&(C[i]), "field1", 42);
-  assert(__CPROVER_get_field(&(C[i]), "field1") == 42);
+  int l;
+  __CPROVER_assume(0 <= l && l < n);
+  __CPROVER_set_field(&(C[l]), "field1", 42);
+  assert(__CPROVER_get_field(&(C[l]), "field1") == 42);
 
-  z = &(C[i]);
+  z = &(C[l]);
   __CPROVER_set_field(z, "field1", 43);
   assert(__CPROVER_get_field(z, "field1") == 43);
 }

regression/goto-analyzer-simplify/simplify-lhs-member/main.c

@@ -11,7 +11,6 @@ void main()
   struct test_struct value;
 
   // Simplify a pointer inside a struct
-  int symbol;
   value.pointer_component = &symbol;
 
   // Simplify
@@ -37,6 +36,6 @@ void main()
   value.array[constant] = 2;
 
   // No simplification
-  int nondet;
-  value.array[nondet] = 3;
+  int nondet2;
+  value.array[nondet2] = 3;
 }

regression/goto-analyzer/pointer-comparison-equality-struct-members/main.c

@@ -22,7 +22,7 @@ int main()
   assert(pa == &(y.a));
   assert(pa != &(y.a));
 
-  int *pb = &(x.b);
-  assert(pb == &(y.a));
-  assert(pb != &(y.a));
+  int *pc = &(x.b);
+  assert(pc == &(y.a));
+  assert(pc != &(y.a));
 }

regression/goto-analyzer/pointer-comparison-equality-struct-members/test-constants.desc

@@ -9,5 +9,5 @@ main.c
 ^\[main.assertion.4\] .* assertion pb != &\(x.a\): SUCCESS
 ^\[main.assertion.5\] .* assertion pa == &\(y.a\): FAILURE
 ^\[main.assertion.6\] .* assertion pa != &\(y.a\): SUCCESS
-^\[main.assertion.7\] .* assertion pb == &\(y.a\): FAILURE
-^\[main.assertion.8\] .* assertion pb != &\(y.a\): SUCCESS
+^\[main.assertion.7\] .* assertion pc == &\(y.a\): FAILURE
+^\[main.assertion.8\] .* assertion pc != &\(y.a\): SUCCESS

regression/goto-analyzer/pointer-comparison-equality-struct-members/test-top-bottom.desc

@@ -9,5 +9,5 @@ main.c
 ^\[main.assertion.4\] .* assertion pb != &\(x.a\): UNKNOWN
 ^\[main.assertion.5\] .* assertion pa == &\(y.a\): UNKNOWN
 ^\[main.assertion.6\] .* assertion pa != &\(y.a\): UNKNOWN
-^\[main.assertion.7\] .* assertion pb == &\(y.a\): UNKNOWN
-^\[main.assertion.8\] .* assertion pb != &\(y.a\): UNKNOWN
+^\[main.assertion.7\] .* assertion pc == &\(y.a\): UNKNOWN
+^\[main.assertion.8\] .* assertion pc != &\(y.a\): UNKNOWN

regression/goto-analyzer/pointer-comparison-equality-struct-members/test-value-set.desc

@@ -9,5 +9,5 @@ main.c
 ^\[main.assertion.4\] .* assertion pb != &\(x.a\): SUCCESS
 ^\[main.assertion.5\] .* assertion pa == &\(y.a\): FAILURE
 ^\[main.assertion.6\] .* assertion pa != &\(y.a\): SUCCESS
-^\[main.assertion.7\] .* assertion pb == &\(y.a\): FAILURE
-^\[main.assertion.8\] .* assertion pb != &\(y.a\): SUCCESS
+^\[main.assertion.7\] .* assertion pc == &\(y.a\): FAILURE
+^\[main.assertion.8\] .* assertion pc != &\(y.a\): SUCCESS

regression/goto-analyzer/sensitivity-test-common-files/array_of_pointer_sensitivity_tests.c

@@ -157,16 +157,16 @@ int main()
   int x = 4;
   int y = 5;
   int *ps[2] = {&x, &y};
-  int i;
+  int l;
   if(nondet > 2)
   {
-    i = 0;
+    l = 0;
   }
   else
   {
-    i = 1;
+    l = 1;
   }
-  *(ps[i]) = 4;
+  *(ps[l]) = 4;
 
   __CPROVER_assert(*ps[0] == 4, "*ps[0]==4");
   __CPROVER_assert(*ps[1] == 4, "*ps[1]==4");

src/ansi-c/c_typecheck_base.cpp

@@ -141,7 +141,19 @@ void c_typecheck_baset::typecheck_symbol(symbolt &symbol)
     if(symbol.is_type)
       typecheck_redefinition_type(existing_symbol, symbol);
     else
+    {
+      if(
+        (!old_it->second.is_static_lifetime || !symbol.is_static_lifetime) &&
+        symbol.type.id() != ID_code)
+      {
+        error().source_location = symbol.location;
+        error() << "redeclaration of '" << symbol.display_name()
+                << "' with no linkage" << eom;
+        throw 0;
+      }
+
       typecheck_redefinition_non_type(existing_symbol, symbol);
+    }
   }
 }
 

unit/compound_block_locations.cpp

@@ -107,9 +107,11 @@ SCENARIO("Compound blocks should have a location")
     "/*  4 */    {                            \n"
     "/*  5 */      int x;                     \n"
     "/*  6 */      if(x)                      \n"
-    "/*  7 */        int x = 1;               \n"
-    "/*  8 */    }                            \n"
-    "/*  9 */  }                              \n",
+    "/*  7 */      {                          \n"
+    "/*  8 */        int x = 1;               \n"
+    "/*  9 */      }                          \n"
+    "/* 10 */    }                            \n"
+    "/* 11 */  }                              \n",
     {{ID_while, 3}, {ID_ifthenelse, 6}});
 
   checker.check(
@@ -233,21 +235,31 @@ SCENARIO("Compound blocks should have a location")
     "/*  4 */    switch(x)                    \n"
     "/*  5 */    {                            \n"
     "/*  6 */    case 1:                      \n"
-    "/*  7 */      int y = 1;                 \n"
-    "/*  8 */      break;                     \n"
-    "/*  9 */    case 2:                      \n"
-    "/* 10 */      int y = 2;                 \n"
-    "/* 11 */      int z = 2;                 \n"
-    "/* 12 */      break;                     \n"
-    "/* 13 */    case 3:                      \n"
-    "/* 14 */      int y = 3;                 \n"
-    "/* 15 */    case 4:                      \n"
-    "/* 16 */      int y = 4;                 \n"
-    "/* 17 */      break;                     \n"
-    "/* 18 */    default:                     \n"
-    "/* 19 */      int y = 5;                 \n"
+    "/*  7 */    {                            \n"
+    "/*  8 */      int y = 1;                 \n"
+    "/*  9 */      break;                     \n"
+    "/* 10 */    }                            \n"
+    "/* 11 */    case 2:                      \n"
+    "/* 12 */    {                            \n"
+    "/* 13 */      int y = 2;                 \n"
+    "/* 14 */      int z = 2;                 \n"
+    "/* 15 */      break;                     \n"
+    "/* 16 */    }                            \n"
+    "/* 17 */    case 3:                      \n"
+    "/* 18 */    {                            \n"
+    "/* 19 */      int y = 3;                 \n"
     "/* 20 */    }                            \n"
-    "/* 21 */  }                              \n",
+    "/* 21 */    case 4:                      \n"
+    "/* 22 */    {                            \n"
+    "/* 23 */      int y = 4;                 \n"
+    "/* 24 */      break;                     \n"
+    "/* 25 */    }                            \n"
+    "/* 26 */    default:                     \n"
+    "/* 27 */    {                            \n"
+    "/* 28 */      int y = 5;                 \n"
+    "/* 29 */    }                            \n"
+    "/* 30 */    }                            \n"
+    "/* 31 */  }                              \n",
     {{ID_switch, 6}});
 }