diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp
index fc8fc87c9b1..9d15ec442e7 100644
--- a/src/ansi-c/c_typecheck_base.cpp
+++ b/src/ansi-c/c_typecheck_base.cpp
@@ -723,16 +723,17 @@ void c_typecheck_baset::typecheck_declaration(
       {
         // section name is not empty, do a bit of parsing
         std::string asm_name = id2string(full_spec.section);
-        if(asm_name[0] != '.')
+
+        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);
         }
-        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
@@ -740,6 +741,7 @@ void c_typecheck_baset::typecheck_declaration(
 
         apply_asm_label(asm_name, symbol);
       }
+
       irep_idt identifier=symbol.name;
       d_it->set_name(identifier);