Revert "Fully interpret __attribute__((always_inline))"
This partly reverts commit 9c93f59593
.
The regression test stays in place, but is now marked as KNOWNBUG.
This commit is contained in:
parent
d20a12e6aa
commit
016ad92b3d
|
@ -1,4 +1,4 @@
|
|||
CORE
|
||||
KNOWNBUG
|
||||
main.c
|
||||
|
||||
^EXIT=0$
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -205,16 +205,6 @@ public:
|
|||
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;
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -36,14 +36,13 @@ public:
|
|||
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 @@ public:
|
|||
|
||||
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 @@ public:
|
|||
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 @@ public:
|
|||
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())
|
||||
|
|
|
@ -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);
|
||||
|
|
|
@ -18,11 +18,9 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#include <util/c_types.h>
|
||||
#include <util/config.h>
|
||||
#include <util/cprover_prefix.h>
|
||||
#include <util/expr_util.h>
|
||||
#include <util/ieee_float.h>
|
||||
#include <util/pointer_offset_size.h>
|
||||
#include <util/pointer_predicates.h>
|
||||
#include <util/replace_symbol.h>
|
||||
#include <util/simplify_expr.h>
|
||||
#include <util/string_constant.h>
|
||||
|
||||
|
@ -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
|
||||
|
|
|
@ -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:
|
||||
|
|
|
@ -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); }
|
||||
|
|
|
@ -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
|
||||
|
|
Loading…
Reference in New Issue