Follow-up to 090790a467: attribute __used__ requires unique names

regression/ansi-c/gcc_attribute_used1/main.c

@@ -0,0 +1,6 @@
+static int foo __attribute__((used)) = 42;
+
+int main()
+{
+  return 0;
+}

regression/ansi-c/gcc_attribute_used1/other.c

@@ -0,0 +1,15 @@
+struct bar
+{
+  char *ptr;
+};
+
+static struct bar foo __attribute__((used))
+__attribute__((__section__(".ref.data")));
+
+static struct bar foo __attribute__((used))
+__attribute__((__section__(".ref.data"))) = {0};
+
+void use_foo()
+{
+  __CPROVER_assert(foo.ptr == 0, "null");
+}

regression/ansi-c/gcc_attribute_used1/test.desc

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

regression/goto-instrument/gcc_attribute_used1/test.desc

@@ -3,7 +3,7 @@ main.c
 
 ^EXIT=0$
 ^SIGNAL=0$
-^[[:space:]]*ASSIGN foo := 42$
+^[[:space:]]*ASSIGN .*foo := 42$
 --
 ^warning: ignoring
 ^CONVERSION ERROR$

src/ansi-c/ansi_c_declaration.cpp

@@ -173,10 +173,6 @@ void ansi_c_declarationt::to_symbol(
         else  if(get_is_extern()) // traditional GCC
           symbol.is_file_local=true;
       }
-
-      // GCC __attribute__((__used__)) - do not treat those as file-local
-      if(get_is_used())
-        symbol.is_file_local = false;
     }
   }
   else // non-function
@@ -190,10 +186,8 @@ void ansi_c_declarationt::to_symbol(
       (!symbol.is_static_lifetime && !get_is_extern()) ||
       get_is_thread_local();
 
-    symbol.is_file_local=
-      symbol.is_macro ||
-      (!get_is_global() && !get_is_extern()) ||
-      (get_is_global() && get_is_static() && !get_is_used()) ||
-      symbol.is_parameter;
+    symbol.is_file_local =
+      symbol.is_macro || (!get_is_global() && !get_is_extern()) ||
+      (get_is_global() && get_is_static()) || symbol.is_parameter;
   }
 }

src/ansi-c/ansi_c_declaration.h

@@ -195,16 +195,6 @@ class ansi_c_declarationt:public exprt
     set(ID_is_weak, is_weak);
   }
 
-  bool get_is_used() const
-  {
-    return get_bool(ID_is_used);
-  }
-
-  void set_is_used(bool is_used)
-  {
-    set(ID_is_used, is_used);
-  }
-
   void to_symbol(
     const ansi_c_declaratort &,
     symbolt &symbol) const;

src/ansi-c/c_typecheck_base.cpp

@@ -19,6 +19,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/std_types.h>
 #include <util/symbol_table_base.h>
 
+#include <goto-programs/name_mangler.h>
+
 #include "ansi_c_declaration.h"
 #include "c_storage_spec.h"
 #include "expr2c.h"
@@ -758,7 +760,6 @@ void c_typecheck_baset::typecheck_declaration(
       declaration.set_is_register(full_spec.is_register);
       declaration.set_is_typedef(full_spec.is_typedef);
       declaration.set_is_weak(full_spec.is_weak);
-      declaration.set_is_used(full_spec.is_used);
 
       symbolt symbol;
       declaration.to_symbol(declarator, symbol);
@@ -788,6 +789,20 @@ void c_typecheck_baset::typecheck_declaration(
         symbol.is_macro=true;
       }
 
+      if(full_spec.is_used && symbol.is_file_local)
+      {
+        // GCC __attribute__((__used__)) - do not treat those as file-local, but
+        // make sure the name is unique
+        symbol.is_file_local = false;
+
+        symbolt symbol_for_renaming = symbol;
+        if(!full_spec.asm_label.empty())
+          symbol_for_renaming.name = full_spec.asm_label;
+        full_spec.asm_label = djb_manglert{}(
+          symbol_for_renaming,
+          id2string(symbol_for_renaming.location.get_file()));
+      }
+
       if(full_spec.section.empty())
         apply_asm_label(full_spec.asm_label, symbol);
       else