diff --git a/regression/goto-instrument/gcc_attribute_used1/main.c b/regression/goto-instrument/gcc_attribute_used1/main.c new file mode 100644 index 00000000000..c479cd5c766 --- /dev/null +++ b/regression/goto-instrument/gcc_attribute_used1/main.c @@ -0,0 +1,10 @@ +#ifdef __GNUC__ +static int foo __attribute__((used)) = 42; +#else +int foo = 42; +#endif + +int main() +{ + return 0; +} diff --git a/regression/goto-instrument/gcc_attribute_used1/test.desc b/regression/goto-instrument/gcc_attribute_used1/test.desc new file mode 100644 index 00000000000..99890290f0e --- /dev/null +++ b/regression/goto-instrument/gcc_attribute_used1/test.desc @@ -0,0 +1,9 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^[[:space:]]*foo = 42;$ +-- +^warning: ignoring +^CONVERSION ERROR$ diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp index 5ece188914f..c1f8956c64e 100644 --- a/src/ansi-c/ansi_c_convert_type.cpp +++ b/src/ansi-c/ansi_c_convert_type.cpp @@ -169,6 +169,8 @@ void ansi_c_convert_typet::read_rec(const typet &type) c_storage_spec.is_register=true; else if(type.id()==ID_weak) c_storage_spec.is_weak=true; + else if(type.id() == ID_used) + c_storage_spec.is_used = true; else if(type.id()==ID_auto) { // ignore diff --git a/src/ansi-c/ansi_c_declaration.cpp b/src/ansi-c/ansi_c_declaration.cpp index 74f05e926b5..5287fa6cfb6 100644 --- a/src/ansi-c/ansi_c_declaration.cpp +++ b/src/ansi-c/ansi_c_declaration.cpp @@ -165,6 +165,10 @@ 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 @@ -181,7 +185,7 @@ void ansi_c_declarationt::to_symbol( symbol.is_file_local= symbol.is_macro || (!get_is_global() && !get_is_extern()) || - (get_is_global() && get_is_static()) || + (get_is_global() && get_is_static() && !get_is_used()) || symbol.is_parameter; } } diff --git a/src/ansi-c/ansi_c_declaration.h b/src/ansi-c/ansi_c_declaration.h index af5db98e32e..4dfdb2b8478 100644 --- a/src/ansi-c/ansi_c_declaration.h +++ b/src/ansi-c/ansi_c_declaration.h @@ -195,6 +195,16 @@ 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; diff --git a/src/ansi-c/c_storage_spec.cpp b/src/ansi-c/c_storage_spec.cpp index 5ed8314bd42..e3e0aa4ef99 100644 --- a/src/ansi-c/c_storage_spec.cpp +++ b/src/ansi-c/c_storage_spec.cpp @@ -32,6 +32,8 @@ void c_storage_spect::read(const typet &type) is_register=true; else if(type.id()==ID_weak) is_weak=true; + else if(type.id() == ID_used) + is_used = true; else if(type.id()==ID_auto) { // ignore diff --git a/src/ansi-c/c_storage_spec.h b/src/ansi-c/c_storage_spec.h index 5b392fe4d05..3061f5ce9af 100644 --- a/src/ansi-c/c_storage_spec.h +++ b/src/ansi-c/c_storage_spec.h @@ -35,13 +35,14 @@ class c_storage_spect is_register=false; is_inline=false; is_weak=false; + is_used = false; alias.clear(); asm_label.clear(); section.clear(); } bool is_typedef, is_extern, is_static, is_register, - is_inline, is_thread_local, is_weak; + is_inline, is_thread_local, is_weak, is_used; // __attribute__((alias("foo"))) irep_idt alias; @@ -59,6 +60,7 @@ class c_storage_spect is_thread_local==other.is_thread_local && is_inline==other.is_inline && is_weak==other.is_weak && + is_used == other.is_used && alias==other.alias && asm_label==other.asm_label && section==other.section; @@ -78,6 +80,7 @@ class c_storage_spect is_inline |=other.is_inline; is_thread_local |=other.is_thread_local; is_weak |=other.is_weak; + is_used |=other.is_used; if(alias.empty()) alias=other.alias; if(asm_label.empty()) diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp index 9d15ec442e7..ae3d38921f2 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/src/ansi-c/c_typecheck_base.cpp @@ -688,6 +688,7 @@ 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(*d_it, symbol); diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y index a6612f2337c..636bb7330b2 100644 --- a/src/ansi-c/parser.y +++ b/src/ansi-c/parser.y @@ -149,6 +149,7 @@ extern char *yyansi_ctext; %token TOK_GCC_ATTRIBUTE_CONSTRUCTOR "constructor" %token TOK_GCC_ATTRIBUTE_DESTRUCTOR "destructor" %token TOK_GCC_ATTRIBUTE_FALLTHROUGH "fallthrough" +%token TOK_GCC_ATTRIBUTE_USED "used" %token TOK_GCC_LABEL "__label__" %token TOK_MSC_ASM "__asm" %token TOK_MSC_BASED "__based" @@ -1544,6 +1545,8 @@ gcc_type_attribute: { $$=$1; set($$, ID_constructor); } | TOK_GCC_ATTRIBUTE_DESTRUCTOR { $$=$1; set($$, ID_destructor); } + | TOK_GCC_ATTRIBUTE_USED + { $$=$1; set($$, ID_used); } ; gcc_attribute: diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l index 45508450351..2d0880d8e77 100644 --- a/src/ansi-c/scanner.l +++ b/src/ansi-c/scanner.l @@ -1582,6 +1582,9 @@ __decltype { if(PARSER.cpp98 && "fallthrough" { BEGIN(GCC_ATTRIBUTE3); loc(); return TOK_GCC_ATTRIBUTE_FALLTHROUGH; } +"used" | +"__used__" { BEGIN(GCC_ATTRIBUTE3); loc(); return TOK_GCC_ATTRIBUTE_USED; } + {ws} { /* ignore */ } {newline} { /* ignore */ } {identifier} { BEGIN(GCC_ATTRIBUTE4); } diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 7f5df683308..bf10417a60b 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -561,6 +561,8 @@ IREP_ID_ONE(noreturn) IREP_ID_TWO(C_noreturn, #noreturn) IREP_ID_ONE(weak) IREP_ID_ONE(is_weak) +IREP_ID_ONE(used) +IREP_ID_ONE(is_used) IREP_ID_TWO(C_spec_loop_invariant, #spec_loop_invariant) IREP_ID_TWO(C_spec_requires, #spec_requires) IREP_ID_TWO(C_spec_ensures, #spec_ensures)