From 8f6bae0ee6ccd3a8e8726dec2d977288e9a6b41c Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 26 May 2018 16:22:36 +0100 Subject: [PATCH] remove a warning about section names --- src/ansi-c/c_typecheck_base.cpp | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) 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);