[SV-COMP'18 19/19] Fixing "identifier XYZ not found" error.

regression/ansi-c/gcc_attributes11/main.c

@@ -0,0 +1,18 @@
+#ifdef __GNUC__
+// example extracted from SV-COMP's ldv-linux-3.4-simple/
+// 32_7_cpp_false-unreach-call_single_drivers-net-phy-dp83640
+static int __attribute__((__section__(".init.text")))
+__attribute__((no_instrument_function)) dp83640_init(void)
+{
+  return 0;
+}
+int init_module(void) __attribute__((alias("dp83640_init")));
+#endif
+
+int main()
+{
+#ifdef __GNUC__
+  dp83640_init();
+#endif
+  return 0;
+}

regression/ansi-c/gcc_attributes11/test.desc

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

regression/ansi-c/gcc_attributes9/main.c

@@ -11,11 +11,23 @@ const char* __attribute__((section("s"))) __attribute__((weak)) bar();
 volatile int __attribute__((__section__(".init.data1"))) txt_heap_base1;
 volatile int __attribute__((__section__(".init.data3"))) txt_heap_base, __attribute__((__section__(".init.data4"))) txt_heap_size;
 
+int __attribute__((__section__(".init.text"))) __attribute__((__cold__))
+__alloc_bootmem_huge_page(void *h);
+int __attribute__((__section__(".init.text"))) __attribute__((__cold__))
+alloc_bootmem_huge_page(void *h);
+int alloc_bootmem_huge_page(void *h)
+  __attribute__((weak, alias("__alloc_bootmem_huge_page")));
+int __alloc_bootmem_huge_page(void *h)
+{
+  return 1;
+}
 #endif
 
 int main()
 {
 #ifdef __GNUC__
+  int r = alloc_bootmem_huge_page(0);
+
   static int __attribute__((section(".data.unlikely"))) __warned;
   __warned=1;
   return __warned;

src/ansi-c/c_typecheck_base.cpp

@@ -708,16 +708,31 @@ void c_typecheck_baset::typecheck_declaration(
 
         // alias function need not have been declared yet, thus
         // can't lookup
-        symbol.value=symbol_exprt(full_spec.alias);
+        // also cater for renaming/placement in sections
+        const auto &renaming_entry = asm_label_map.find(full_spec.alias);
+        if(renaming_entry == asm_label_map.end())
+          symbol.value = symbol_exprt(full_spec.alias);
+        else
+          symbol.value = symbol_exprt(renaming_entry->second);
         symbol.is_macro=true;
       }
 
       if(full_spec.section.empty())
         apply_asm_label(full_spec.asm_label, symbol);
       else
       {
-        std::string asm_name;
-        asm_name=id2string(full_spec.section)+"$$";
+        // section name is not empty, do a bit of parsing
+        std::string asm_name = id2string(full_spec.section);
+        if(asm_name[0] != '.')
+        {
+          warning().source_location = symbol.location;
+          warning() << "section name `" << asm_name
+                    << "' expected to start with `.'" << eom;
+        }
+        std::string::size_type primary_section = asm_name.find('.', 1);
+        if(primary_section != std::string::npos)
+          asm_name.resize(primary_section);
+        asm_name += "$$";
         if(!full_spec.asm_label.empty())
           asm_name+=id2string(full_spec.asm_label);
         else

src/ansi-c/expr2c.cpp

@@ -8,6 +8,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "expr2c.h"
 
+#include <algorithm>
 #include <cassert>
 #include <cctype>
 #include <cstdio>
@@ -89,6 +90,9 @@ static std::string clean_identifier(const irep_idt &id)
         *it2='_';
   }
 
+  // rewrite . as used in ELF section names
+  std::replace(dest.begin(), dest.end(), '.', '_');
+
   return dest;
 }