diff --git a/regression/cpp/virtual1/main.cpp b/regression/cpp/virtual1/main.cpp index 911f5550588..36cc605b23e 100644 --- a/regression/cpp/virtual1/main.cpp +++ b/regression/cpp/virtual1/main.cpp @@ -1,5 +1,5 @@ -#include -#include +#include +#include class base { diff --git a/regression/cpp/virtual1/test.desc b/regression/cpp/virtual1/test.desc index 5893356edf6..a003b07b93c 100644 --- a/regression/cpp/virtual1/test.desc +++ b/regression/cpp/virtual1/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.cpp ^EXIT=0$ diff --git a/src/cpp/cpp_typecheck_compound_type.cpp b/src/cpp/cpp_typecheck_compound_type.cpp index 77a445777d8..f2be6ebe189 100644 --- a/src/cpp/cpp_typecheck_compound_type.cpp +++ b/src/cpp/cpp_typecheck_compound_type.cpp @@ -356,8 +356,7 @@ void cpp_typecheckt::typecheck_compound_declarator( throw 0; } - if(is_constructor && - base_name!=id2string(symbol.base_name)) + if(is_constructor && base_name != symbol.base_name) { error().source_location=cpp_name.source_location(); error() << "member function must return a value or void" << eom; @@ -425,7 +424,7 @@ void cpp_typecheckt::typecheck_compound_declarator( } if(is_typedef) - component.set("is_type", true); + component.set(ID_is_type, true); if(is_mutable) component.set("is_mutable", true); @@ -448,7 +447,7 @@ void cpp_typecheckt::typecheck_compound_declarator( virtual_name+="$const"; if(has_volatile(method_qualifier)) - virtual_name+="$virtual"; + virtual_name += "$volatile"; if(component.type().get(ID_return_type)==ID_destructor) virtual_name="@dtor"; @@ -491,22 +490,18 @@ void cpp_typecheckt::typecheck_compound_declarator( component.type().set("#virtual_name", virtual_name); // Check if it is a pure virtual method - if(is_virtual) + if(value.is_not_nil() && value.id() == ID_constant) { - if(value.is_not_nil() && value.id()==ID_constant) + mp_integer i; + to_integer(value, i); + if(i!=0) { - mp_integer i; - to_integer(value, i); - if(i!=0) - { - error().source_location=declarator.name().source_location(); - error() << "expected 0 to mark pure virtual method, got " - << i << eom; - throw 0; - } - component.set("is_pure_virtual", true); - value.make_nil(); + error().source_location = declarator.name().source_location(); + error() << "expected 0 to mark pure virtual method, got " << i << eom; + throw 0; } + component.set("is_pure_virtual", true); + value.make_nil(); } typecheck_member_function( @@ -615,47 +610,36 @@ void cpp_typecheckt::typecheck_compound_declarator( // do the body of the function typecast_exprt late_cast( + lookup(args[0].get(ID_C_identifier)).symbol_expr(), to_code_type(component.type()).parameters()[0].type()); - late_cast.op0()= - namespacet(symbol_table).lookup( - args[0].get(ID_C_identifier)).symbol_expr(); + side_effect_expr_function_callt expr_call; + expr_call.function() = + symbol_exprt(component.get_name(), component.type()); + expr_call.arguments().reserve(args.size()); + expr_call.arguments().push_back(late_cast); + + for(const auto &arg : args) + { + expr_call.arguments().push_back( + lookup(arg.get(ID_C_identifier)).symbol_expr()); + } if(code_type.return_type().id()!=ID_empty && code_type.return_type().id()!=ID_destructor) { - side_effect_expr_function_callt expr_call; - expr_call.function()= - symbol_exprt(component.get_name(), component.type()); expr_call.type()=to_code_type(component.type()).return_type(); - expr_call.arguments().reserve(args.size()); - expr_call.arguments().push_back(late_cast); + exprt already_typechecked(ID_already_typechecked); + already_typechecked.move_to_operands(expr_call); - for(std::size_t i=1; i < args.size(); i++) - { - expr_call.arguments().push_back( - namespacet(symbol_table).lookup( - args[i].get(ID_C_identifier)).symbol_expr()); - } - - func_symb.value=code_returnt(expr_call); + func_symb.value = code_returnt(already_typechecked).make_block(); } else { - code_function_callt code_func; - code_func.function()= - symbol_exprt(component.get_name(), component.type()); - code_func.arguments().reserve(args.size()); - code_func.arguments().push_back(late_cast); + exprt already_typechecked(ID_already_typechecked); + already_typechecked.move_to_operands(expr_call); - for(std::size_t i=1; i < args.size(); i++) - { - code_func.arguments().push_back( - namespacet(symbol_table).lookup( - args[i].get(ID_C_identifier)).symbol_expr()); - } - - func_symb.value=code_func; + func_symb.value = code_expressiont(already_typechecked).make_block(); } // add this new function to the list of components @@ -671,6 +655,8 @@ void cpp_typecheckt::typecheck_compound_declarator( CHECK_RETURN(!failed); } + put_compound_into_scope(new_compo); + // next base virtual_bases.erase(virtual_bases.begin()); } diff --git a/src/cpp/cpp_typecheck_constructor.cpp b/src/cpp/cpp_typecheck_constructor.cpp index 05dde093467..4c4edfad22b 100644 --- a/src/cpp/cpp_typecheck_constructor.cpp +++ b/src/cpp/cpp_typecheck_constructor.cpp @@ -297,12 +297,10 @@ void cpp_typecheckt::default_cpctor( cppname.move_to_sub(name); const symbolt &virtual_table_symbol_type = - namespacet(symbol_table).lookup( - mem_it->type().subtype().get(ID_identifier)); + lookup(mem_it->type().subtype().get(ID_identifier)); - const symbolt &virtual_table_symbol_var = - namespacet(symbol_table).lookup( - id2string(virtual_table_symbol_type.name) + "@" + + const symbolt &virtual_table_symbol_var = lookup( + id2string(virtual_table_symbol_type.name) + "@" + id2string(symbol.name)); exprt var=virtual_table_symbol_var.symbol_expr(); diff --git a/src/cpp/cpp_typecheck_destructor.cpp b/src/cpp/cpp_typecheck_destructor.cpp index acfae7e92c8..e985f16b7de 100644 --- a/src/cpp/cpp_typecheck_destructor.cpp +++ b/src/cpp/cpp_typecheck_destructor.cpp @@ -89,12 +89,11 @@ codet cpp_typecheckt::dtor(const symbolt &symbol) cppname.move_to_sub(name); const symbolt &virtual_table_symbol_type = - namespacet(symbol_table).lookup( - cit->type().subtype().get(ID_identifier)); + lookup(cit->type().subtype().get(ID_identifier)); - const symbolt &virtual_table_symbol_var = - namespacet(symbol_table).lookup( - id2string(virtual_table_symbol_type.name)+"@"+id2string(symbol.name)); + const symbolt &virtual_table_symbol_var = lookup( + id2string(virtual_table_symbol_type.name) + "@" + + id2string(symbol.name)); exprt var=virtual_table_symbol_var.symbol_expr(); address_of_exprt address(var); diff --git a/src/cpp/cpp_typecheck_function.cpp b/src/cpp/cpp_typecheck_function.cpp index 8081368e290..454ba8161a0 100644 --- a/src/cpp/cpp_typecheck_function.cpp +++ b/src/cpp/cpp_typecheck_function.cpp @@ -34,6 +34,11 @@ void cpp_typecheckt::convert_parameter( parameter.set_identifier(identifier); + // the parameter may already have been set up if dealing with virtual methods + const symbolt *check_symbol; + if(!lookup(identifier, check_symbol)) + return; + symbolt symbol; symbol.name=identifier; @@ -93,7 +98,12 @@ void cpp_typecheckt::convert_function(symbolt &symbol) assert(symbol.value.id()==ID_code); assert(symbol.value.get(ID_statement)==ID_block); - symbol.value.copy_to_operands(dtor(msymb)); + if( + !symbol.value.has_operands() || !symbol.value.op0().has_operands() || + symbol.value.op0().op0().id() != ID_already_typechecked) + { + symbol.value.copy_to_operands(dtor(msymb)); + } } // enter appropriate scope @@ -168,9 +178,9 @@ irep_idt cpp_typecheckt::function_identifier(const typet &type) const typet &pointer=it->type(); const typet &symbol =pointer.subtype(); if(symbol.get_bool(ID_C_constant)) - result+="const$"; + result += "$const"; if(symbol.get_bool(ID_C_volatile)) - result+="volatile$"; + result += "$volatile"; result+="this"; first=false; it++; diff --git a/src/cpp/cpp_typecheck_virtual_table.cpp b/src/cpp/cpp_typecheck_virtual_table.cpp index 830bcd8a8b5..f8ffa0dd8c3 100644 --- a/src/cpp/cpp_typecheck_virtual_table.cpp +++ b/src/cpp/cpp_typecheck_virtual_table.cpp @@ -61,10 +61,9 @@ void cpp_typecheckt::do_virtual_table(const symbolt &symbol) { const std::map &value_map=cit->second; - const symbolt &late_cast_symb=namespacet(symbol_table).lookup(cit->first); - const symbolt &vt_symb_type= - namespacet(symbol_table).lookup( - "virtual_table::"+id2string(late_cast_symb.name)); + const symbolt &late_cast_symb = lookup(cit->first); + const symbolt &vt_symb_type = + lookup("virtual_table::" + id2string(late_cast_symb.name)); symbolt vt_symb_var; vt_symb_var.name=