diff --git a/regression/ansi-c/always_inline1/test.desc b/regression/ansi-c/always_inline1/test.desc index c6ac7d7513d..585aa7c0ad5 100644 --- a/regression/ansi-c/always_inline1/test.desc +++ b/regression/ansi-c/always_inline1/test.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG main.c ^EXIT=0$ diff --git a/regression/ansi-c/always_inline2/main.c b/regression/ansi-c/always_inline2/main.c new file mode 100644 index 00000000000..67e8593149b --- /dev/null +++ b/regression/ansi-c/always_inline2/main.c @@ -0,0 +1,16 @@ +static inline __attribute__((__always_inline__)) int func(int val) +{ + return val; +} + +static inline int func2(int *p) +{ + // the typecast, although redundant, is essential to show the problem + return func(*(int*)p); +} + +int main() +{ + int x; + return func2(&x); +} diff --git a/regression/ansi-c/always_inline2/test.desc b/regression/ansi-c/always_inline2/test.desc new file mode 100644 index 00000000000..0e1ed863bc1 --- /dev/null +++ b/regression/ansi-c/always_inline2/test.desc @@ -0,0 +1,8 @@ +CORE gcc-only +main.c + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +^CONVERSION ERROR$ diff --git a/regression/ansi-c/always_inline3/main.c b/regression/ansi-c/always_inline3/main.c new file mode 100644 index 00000000000..c72fde139b2 --- /dev/null +++ b/regression/ansi-c/always_inline3/main.c @@ -0,0 +1,12 @@ +static inline __attribute__((__always_inline__)) int func(int val) +{ + if(val > 0) + return func(val - 1); + return 0; +} + +int main() +{ + int x; + return func(x); +} diff --git a/regression/ansi-c/always_inline3/test.desc b/regression/ansi-c/always_inline3/test.desc new file mode 100644 index 00000000000..0e1ed863bc1 --- /dev/null +++ b/regression/ansi-c/always_inline3/test.desc @@ -0,0 +1,8 @@ +CORE gcc-only +main.c + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +^CONVERSION ERROR$ diff --git a/regression/ansi-c/always_inline4/main.c b/regression/ansi-c/always_inline4/main.c new file mode 100644 index 00000000000..1e52a46071a --- /dev/null +++ b/regression/ansi-c/always_inline4/main.c @@ -0,0 +1,14 @@ +extern int func_alias(int val) __asm__("" "func"); + +static inline __attribute__((__always_inline__)) int func(int val) +{ + if(val > 0) + return func_alias(val - 1); + return 0; +} + +int main() +{ + int x; + return func(x); +} diff --git a/regression/ansi-c/always_inline4/test.desc b/regression/ansi-c/always_inline4/test.desc new file mode 100644 index 00000000000..0e1ed863bc1 --- /dev/null +++ b/regression/ansi-c/always_inline4/test.desc @@ -0,0 +1,8 @@ +CORE gcc-only +main.c + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +^CONVERSION ERROR$ diff --git a/regression/ansi-c/always_inline5/main.c b/regression/ansi-c/always_inline5/main.c new file mode 100644 index 00000000000..52998788bda --- /dev/null +++ b/regression/ansi-c/always_inline5/main.c @@ -0,0 +1,12 @@ +static inline +__attribute__((__section__(".init"))) __attribute__((__always_inline__)) +int func(int val) +{ + return val + 1; +} + +int main() +{ + int x; + return func(x); +} diff --git a/regression/ansi-c/always_inline5/test.desc b/regression/ansi-c/always_inline5/test.desc new file mode 100644 index 00000000000..0e1ed863bc1 --- /dev/null +++ b/regression/ansi-c/always_inline5/test.desc @@ -0,0 +1,8 @@ +CORE gcc-only +main.c + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +^CONVERSION ERROR$ diff --git a/regression/ansi-c/always_inline6/main.c b/regression/ansi-c/always_inline6/main.c new file mode 100644 index 00000000000..107e345e992 --- /dev/null +++ b/regression/ansi-c/always_inline6/main.c @@ -0,0 +1,10 @@ +static inline __attribute__((__always_inline__)) int func(int val, ...) +{ + return val + 1; +} + +int main() +{ + int x; + return func(x, x); +} diff --git a/regression/ansi-c/always_inline6/test.desc b/regression/ansi-c/always_inline6/test.desc new file mode 100644 index 00000000000..0e1ed863bc1 --- /dev/null +++ b/regression/ansi-c/always_inline6/test.desc @@ -0,0 +1,8 @@ +CORE gcc-only +main.c + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +^CONVERSION ERROR$ diff --git a/regression/ansi-c/always_inline7/main.c b/regression/ansi-c/always_inline7/main.c new file mode 100644 index 00000000000..26bc49ccb94 --- /dev/null +++ b/regression/ansi-c/always_inline7/main.c @@ -0,0 +1,11 @@ +static inline __attribute__((__always_inline__)) int func(int val) +{ + int local = val; + return local; +} + +int main() +{ + int x; + return func(x); +} diff --git a/regression/ansi-c/always_inline7/test.desc b/regression/ansi-c/always_inline7/test.desc new file mode 100644 index 00000000000..0e1ed863bc1 --- /dev/null +++ b/regression/ansi-c/always_inline7/test.desc @@ -0,0 +1,8 @@ +CORE gcc-only +main.c + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +^CONVERSION ERROR$ diff --git a/regression/ansi-c/always_inline8/main.c b/regression/ansi-c/always_inline8/main.c new file mode 100644 index 00000000000..ca53659d773 --- /dev/null +++ b/regression/ansi-c/always_inline8/main.c @@ -0,0 +1,10 @@ +static inline __attribute__((__always_inline__)) int func(int val) +{ + return (__typeof__(val))42; +} + +int main() +{ + int x; + return func(x); +} diff --git a/regression/ansi-c/always_inline8/test.desc b/regression/ansi-c/always_inline8/test.desc new file mode 100644 index 00000000000..0e1ed863bc1 --- /dev/null +++ b/regression/ansi-c/always_inline8/test.desc @@ -0,0 +1,8 @@ +CORE gcc-only +main.c + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +^CONVERSION ERROR$ diff --git a/regression/ansi-c/always_inline9/main.c b/regression/ansi-c/always_inline9/main.c new file mode 100644 index 00000000000..2489dd94cc5 --- /dev/null +++ b/regression/ansi-c/always_inline9/main.c @@ -0,0 +1,11 @@ +static inline __attribute__((__always_inline__)) int func(int val) +{ + val = val + 1; + return val; +} + +int main() +{ + int x; + return func(x); +} diff --git a/regression/ansi-c/always_inline9/test.desc b/regression/ansi-c/always_inline9/test.desc new file mode 100644 index 00000000000..0e1ed863bc1 --- /dev/null +++ b/regression/ansi-c/always_inline9/test.desc @@ -0,0 +1,8 @@ +CORE gcc-only +main.c + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +^CONVERSION ERROR$ diff --git a/regression/cbmc/always_inline1/main.c b/regression/cbmc/always_inline1/main.c new file mode 100644 index 00000000000..118aacfd4ef --- /dev/null +++ b/regression/cbmc/always_inline1/main.c @@ -0,0 +1,24 @@ +#include + +#ifndef __GNUC__ +#define __attribute__(x) +#endif + +static inline __attribute__((__always_inline__)) void func(int *val) +{ + *val = 1; + return; +} + +static inline int func2(int *p) +{ + func(p); + return *p; +} + +int main() +{ + int x; + assert(func2(&x) == 1); + return 0; +} diff --git a/regression/cbmc/always_inline1/test.desc b/regression/cbmc/always_inline1/test.desc new file mode 100644 index 00000000000..9efefbc7362 --- /dev/null +++ b/regression/cbmc/always_inline1/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc/always_inline2/main.c b/regression/cbmc/always_inline2/main.c new file mode 100644 index 00000000000..837d76fa0d2 --- /dev/null +++ b/regression/cbmc/always_inline2/main.c @@ -0,0 +1,30 @@ +#include + +#ifndef __GNUC__ +#define __attribute__(x) +#endif + +static inline __attribute__((__always_inline__)) int func(int *val) +{ + switch(*val) + { + case 1: + return *val + 1; + case 2: + return *val + 2; + } + + return *val; +} + +static inline int func2(int *p) +{ + return func(p); +} + +int main() +{ + int x = 1; + assert(func2(&x) == 2); + return 0; +} diff --git a/regression/cbmc/always_inline2/test.desc b/regression/cbmc/always_inline2/test.desc new file mode 100644 index 00000000000..9efefbc7362 --- /dev/null +++ b/regression/cbmc/always_inline2/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc/always_inline3/main.c b/regression/cbmc/always_inline3/main.c new file mode 100644 index 00000000000..8dc962ca613 --- /dev/null +++ b/regression/cbmc/always_inline3/main.c @@ -0,0 +1,32 @@ +#include + +#ifndef __GNUC__ +#define __attribute__(x) +#endif + +static inline __attribute__((__always_inline__)) void func(int *val) +{ + if(*val < 0) + { + *val = 1; + return; + } + else + { + *val = 1; + return; + } +} + +static inline int func2(int *p) +{ + func(p); + return *p; +} + +int main() +{ + int x; + assert(func2(&x) == 1); + return 0; +} diff --git a/regression/cbmc/always_inline3/test.desc b/regression/cbmc/always_inline3/test.desc new file mode 100644 index 00000000000..9efefbc7362 --- /dev/null +++ b/regression/cbmc/always_inline3/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp index cc40c75214a..e30503ae627 100644 --- a/src/ansi-c/ansi_c_convert_type.cpp +++ b/src/ansi-c/ansi_c_convert_type.cpp @@ -171,8 +171,6 @@ void ansi_c_convert_typet::read_rec(const typet &type) c_storage_spec.is_weak=true; else if(type.id() == ID_used) c_storage_spec.is_used = true; - else if(type.id() == ID_always_inline) - c_storage_spec.is_always_inline = 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 d757d119dc0..5287fa6cfb6 100644 --- a/src/ansi-c/ansi_c_declaration.cpp +++ b/src/ansi-c/ansi_c_declaration.cpp @@ -81,8 +81,6 @@ void ansi_c_declarationt::output(std::ostream &out) const out << " is_extern"; if(get_is_static_assert()) out << " is_static_assert"; - if(get_is_always_inline()) - out << " is_always_inline"; out << "\n"; out << "Type: " << type().pretty() << "\n"; @@ -166,9 +164,6 @@ void ansi_c_declarationt::to_symbol( symbol.is_extern=false; else if(get_is_extern()) // traditional GCC symbol.is_file_local=true; - - if(get_is_always_inline()) - symbol.is_macro = true; } // GCC __attribute__((__used__)) - do not treat those as file-local diff --git a/src/ansi-c/ansi_c_declaration.h b/src/ansi-c/ansi_c_declaration.h index 3cbe9b52eb1..4dfdb2b8478 100644 --- a/src/ansi-c/ansi_c_declaration.h +++ b/src/ansi-c/ansi_c_declaration.h @@ -205,16 +205,6 @@ class ansi_c_declarationt:public exprt set(ID_is_used, is_used); } - bool get_is_always_inline() const - { - return get_bool(ID_is_always_inline); - } - - void set_is_always_inline(bool is_always_inline) - { - set(ID_is_always_inline, is_always_inline); - } - 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 008a0098e4e..e3e0aa4ef99 100644 --- a/src/ansi-c/c_storage_spec.cpp +++ b/src/ansi-c/c_storage_spec.cpp @@ -34,8 +34,6 @@ void c_storage_spect::read(const typet &type) is_weak=true; else if(type.id() == ID_used) is_used = true; - else if(type.id() == ID_always_inline) - is_always_inline = 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 e2ff9f2fe69..3061f5ce9af 100644 --- a/src/ansi-c/c_storage_spec.h +++ b/src/ansi-c/c_storage_spec.h @@ -36,14 +36,13 @@ class c_storage_spect is_inline=false; is_weak=false; is_used = false; - is_always_inline = 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_used, is_always_inline; + bool is_typedef, is_extern, is_static, is_register, + is_inline, is_thread_local, is_weak, is_used; // __attribute__((alias("foo"))) irep_idt alias; @@ -54,7 +53,6 @@ class c_storage_spect bool operator==(const c_storage_spect &other) const { - // clang-format off return is_typedef==other.is_typedef && is_extern==other.is_extern && is_static==other.is_static && @@ -63,11 +61,9 @@ class c_storage_spect is_inline==other.is_inline && is_weak==other.is_weak && is_used == other.is_used && - is_always_inline == other.is_always_inline && alias==other.alias && asm_label==other.asm_label && section==other.section; - // clang-format on } bool operator!=(const c_storage_spect &other) const @@ -85,7 +81,6 @@ class c_storage_spect is_thread_local |=other.is_thread_local; is_weak |=other.is_weak; is_used |=other.is_used; - is_always_inline |= other.is_always_inline; 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 512d790ba4d..ae3d38921f2 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/src/ansi-c/c_typecheck_base.cpp @@ -689,7 +689,6 @@ void c_typecheck_baset::typecheck_declaration( declaration.set_is_typedef(full_spec.is_typedef); declaration.set_is_weak(full_spec.is_weak); declaration.set_is_used(full_spec.is_used); - declaration.set_is_always_inline(full_spec.is_always_inline); symbolt symbol; declaration.to_symbol(*d_it, symbol); diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 4c8b9e838fb..a93073133aa 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -18,11 +18,9 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include -#include #include #include @@ -1920,10 +1918,7 @@ void c_typecheck_baset::typecheck_side_effect_function_call( if(entry!=asm_label_map.end()) identifier=entry->second; - symbol_tablet::symbolst::const_iterator sym_entry = - symbol_table.symbols.find(identifier); - - if(sym_entry == symbol_table.symbols.end()) + if(symbol_table.symbols.find(identifier)==symbol_table.symbols.end()) { // This is an undeclared function. // Is this a builtin? @@ -1965,87 +1960,6 @@ void c_typecheck_baset::typecheck_side_effect_function_call( warning() << "function `" << identifier << "' is not declared" << eom; } } - else if( - sym_entry->second.type.get_bool(ID_C_inlined) && - sym_entry->second.is_macro && sym_entry->second.value.is_not_nil()) - { - // calling a function marked as always_inline - const symbolt &func_sym = sym_entry->second; - const code_typet &func_type = to_code_type(func_sym.type); - - replace_symbolt replace; - - const code_typet::parameterst ¶meters = func_type.parameters(); - auto p_it = parameters.begin(); - for(const auto &arg : expr.arguments()) - { - if(p_it == parameters.end()) - { - // we don't support varargs with always_inline - err_location(f_op); - error() << "function call has additional arguments, " - << "cannot apply always_inline" << eom; - throw 0; - } - - irep_idt p_id = p_it->get_identifier(); - if(p_id.empty()) - { - p_id = id2string(func_sym.base_name) + "::" + - id2string(p_it->get_base_name()); - } - replace.insert(p_id, arg); - - ++p_it; - } - - if(p_it != parameters.end()) - { - err_location(f_op); - error() << "function call has missing arguments, " - << "cannot apply always_inline" << eom; - throw 0; - } - - codet body = to_code(func_sym.value); - replace(body); - - side_effect_exprt side_effect_expr( - ID_statement_expression, func_type.return_type()); - body.make_block(); - - // simulates parts of typecheck_function_body - typet cur_return_type = return_type; - return_type = func_type.return_type(); - typecheck_code(body); - return_type.swap(cur_return_type); - - // replace final return by an ID_expression - codet &last = to_code_block(body).find_last_statement(); - - if(last.get_statement() == ID_return) - last.set_statement(ID_expression); - - // NOLINTNEXTLINE(whitespace/braces) - const bool has_returns = has_subexpr(body, [&](const exprt &e) { - return e.id() == ID_code && to_code(e).get_statement() == ID_return; - }); - if(has_returns) - { - // we don't support multiple return statements with always_inline - err_location(last); - error() << "function has multiple return statements, " - << "cannot apply always_inline" << eom; - throw 0; - } - - side_effect_expr.copy_to_operands(body); - typecheck_side_effect_statement_expression(side_effect_expr); - - expr.swap(side_effect_expr); - - return; - } } // typecheck it now diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y index 164eb34eb09..636bb7330b2 100644 --- a/src/ansi-c/parser.y +++ b/src/ansi-c/parser.y @@ -150,7 +150,6 @@ extern char *yyansi_ctext; %token TOK_GCC_ATTRIBUTE_DESTRUCTOR "destructor" %token TOK_GCC_ATTRIBUTE_FALLTHROUGH "fallthrough" %token TOK_GCC_ATTRIBUTE_USED "used" -%token TOK_GCC_ATTRIBUTE_ALWAYS_INLINE "always_inline" %token TOK_GCC_LABEL "__label__" %token TOK_MSC_ASM "__asm" %token TOK_MSC_BASED "__based" @@ -1548,8 +1547,6 @@ gcc_type_attribute: { $$=$1; set($$, ID_destructor); } | TOK_GCC_ATTRIBUTE_USED { $$=$1; set($$, ID_used); } - | TOK_GCC_ATTRIBUTE_ALWAYS_INLINE - { $$=$1; set($$, ID_always_inline); } ; gcc_attribute: diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l index 61b69ff98d7..765a30fbf0f 100644 --- a/src/ansi-c/scanner.l +++ b/src/ansi-c/scanner.l @@ -1590,9 +1590,6 @@ __decltype { if(PARSER.cpp98 && "used" | "__used__" { BEGIN(GCC_ATTRIBUTE3); loc(); return TOK_GCC_ATTRIBUTE_USED; } -"always_inline" | -"__always_inline__" { BEGIN(GCC_ATTRIBUTE3); loc(); return TOK_GCC_ATTRIBUTE_ALWAYS_INLINE; } - {ws} { /* ignore */ } {newline} { /* ignore */ } {identifier} { BEGIN(GCC_ATTRIBUTE4); } diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index a0899029370..daa9fa47c42 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -673,8 +673,6 @@ IREP_ID_TWO(C_abstract, #abstract) IREP_ID_ONE(synthetic) IREP_ID_ONE(interface) IREP_ID_TWO(C_must_not_throw, #must_not_throw) -IREP_ID_ONE(always_inline) -IREP_ID_ONE(is_always_inline) IREP_ID_ONE(is_inner_class) // Projects depending on this code base that wish to extend the list of diff --git a/src/util/replace_symbol.cpp b/src/util/replace_symbol.cpp index 6eb8b19563b..e568758661f 100644 --- a/src/util/replace_symbol.cpp +++ b/src/util/replace_symbol.cpp @@ -100,10 +100,6 @@ bool replace_symbolt::replace( if(c_sizeof_type.is_not_nil() && have_to_replace(c_sizeof_type)) result &= replace(static_cast(dest.add(ID_C_c_sizeof_type))); - const typet &type_arg = static_cast(dest.find(ID_type_arg)); - if(type_arg.is_not_nil() && have_to_replace(type_arg)) - result &= replace(static_cast(dest.add(ID_type_arg))); - const typet &va_arg_type = static_cast(dest.find(ID_C_va_arg_type)); if(va_arg_type.is_not_nil() && have_to_replace(va_arg_type)) @@ -140,12 +136,6 @@ bool replace_symbolt::have_to_replace(const exprt &dest) const if(have_to_replace(static_cast(c_sizeof_type))) return true; - const irept &type_arg = dest.find(ID_type_arg); - - if(type_arg.is_not_nil()) - if(have_to_replace(static_cast(type_arg))) - return true; - const irept &va_arg_type=dest.find(ID_C_va_arg_type); if(va_arg_type.is_not_nil())