C front-end: Record extern declarations in current scope

regression/cbmc/extern1/main.c

@@ -0,0 +1,31 @@
+#include <stdio.h>
+#include <assert.h>
+
+int some_global = 10;
+
+void shadow()
+{
+  int some_global = 5;
+
+  printf("local: %d\n", some_global);
+  {
+    int some_global = 0;
+    ++some_global;
+    printf("local2: %d\n", some_global);
+  }
+
+  printf("local: %d\n", some_global);
+  {
+    extern int some_global;
+    ++some_global;
+    printf("global: %d\n", some_global);
+    assert(some_global == 11);
+  }
+
+  assert(some_global == 5);
+}
+
+int main(void)
+{
+  shadow();
+}

regression/cbmc/extern1/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--

regression/cbmc/extern2/main.c

@@ -0,0 +1,20 @@
+#include <stdio.h>
+#include <assert.h>
+
+int param;
+void function(int param)
+{
+  printf("%d\n", param);
+  {
+    extern int param;
+    printf("%d\n", param);
+    assert(param == 2);
+  }
+  assert(param == 1);
+}
+
+int main(void)
+{
+  param = 2;
+  function(1);
+}

regression/cbmc/extern2/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--

src/ansi-c/ansi_c_parser.cpp

@@ -8,8 +8,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "ansi_c_parser.h"
 
-#include <iostream>
-
 #include "c_storage_spec.h"
 
 ansi_c_parsert ansi_c_parser;
@@ -35,8 +33,6 @@ ansi_c_id_classt ansi_c_parsert::lookup(
 
     if(n_it!=it->name_map.end())
     {
-      assert(id2string(n_it->second.prefixed_name)==
-             it->prefix+id2string(scope_name));
       identifier=n_it->second.prefixed_name;
       return n_it->second.id_class;
     }
@@ -150,6 +146,9 @@ void ansi_c_parsert::add_declarator(
     ansi_c_identifiert &identifier=scope.name_map[base_name];
     identifier.id_class=id_class;
     identifier.prefixed_name=prefixed_name;
+
+    if(force_root_scope)
+      current_scope().name_map[base_name] = identifier;
   }
 
   ansi_c_declaration.declarators().push_back(new_declarator);

src/ansi-c/expr2c.cpp

@@ -89,7 +89,7 @@ void expr2ct::get_shorthands(const exprt &expr)
   find_symbols_sett symbols;
   find_symbols(expr, symbols);
 
-  // avoid renaming parameters
+  // avoid renaming parameters, if possible
   for(find_symbols_sett::const_iterator
       it=symbols.begin();
       it!=symbols.end();
@@ -103,7 +103,16 @@ void expr2ct::get_shorthands(const exprt &expr)
 
     irep_idt sh=id_shorthand(*it);
 
-    ns_collision[symbol->location.get_function()].insert(sh);
+    std::string func = id2string(*it);
+    func = func.substr(0, func.rfind("::"));
+
+    // if there is a global symbol of the same name as the shorthand (even if
+    // not present in this particular expression) then there is a collision
+    const symbolt *global_symbol;
+    if(!ns.lookup(sh, global_symbol))
+      sh = func + "$$" + id2string(sh);
+
+    ns_collision[func].insert(sh);
 
     if(!shorthands.insert(std::make_pair(*it, sh)).second)
       UNREACHABLE;
@@ -125,6 +134,8 @@ void expr2ct::get_shorthands(const exprt &expr)
 
     if(!has_collision)
     {
+      // if there is a global symbol of the same name as the shorthand (even if
+      // not present in this particular expression) then there is a collision
       const symbolt *symbol;
       has_collision=!ns.lookup(sh, symbol);
     }