Typecheck friend type declarations
This does not yet include typechecking of friend methods. Includes a fix to permit rvalue conversion to const references, which ensures unambiguous resolution for member functions.
This commit is contained in:
parent
311c98ac63
commit
ebb3ea4cdd
|
@ -1,5 +1,3 @@
|
|||
#include <cassert>
|
||||
|
||||
template <int W>
|
||||
class sc_uint {
|
||||
public:
|
||||
|
@ -41,8 +39,8 @@ int main(int argc, char** argv)
|
|||
x.test1();
|
||||
x.test2();
|
||||
|
||||
assert(x.to_uint() == 1);
|
||||
assert(x.to_uint() == 2);
|
||||
__CPROVER_assert(x.to_uint() == 1, "");
|
||||
__CPROVER_assert(x.to_uint() == 2, "");
|
||||
|
||||
return 0;
|
||||
}
|
||||
|
|
|
@ -1,5 +1,3 @@
|
|||
#include <cassert>
|
||||
|
||||
template <int W>
|
||||
class sc_uint {
|
||||
public:
|
||||
|
@ -56,7 +54,7 @@ int main(int argc, char** argv)
|
|||
z += y;
|
||||
|
||||
sc_uint<10> w(3);
|
||||
assert(z == w);
|
||||
__CPROVER_assert(z == w, "");
|
||||
|
||||
return 0;
|
||||
}
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
KNOWNBUG
|
||||
CORE
|
||||
main.cpp
|
||||
|
||||
^EXIT=0$
|
||||
|
|
|
@ -1,5 +1,3 @@
|
|||
#include <cassert>
|
||||
|
||||
template<class T>
|
||||
class myclass
|
||||
{
|
||||
|
@ -20,5 +18,5 @@ int main(int argc, char** argv)
|
|||
myclass<int> x(0);
|
||||
myclass<int> y(1);
|
||||
x = y;
|
||||
assert(x == y);
|
||||
__CPROVER_assert(x == y, "");
|
||||
}
|
||||
|
|
|
@ -1,5 +1,3 @@
|
|||
#include <cassert>
|
||||
|
||||
template<class T>
|
||||
class myclass
|
||||
{
|
||||
|
@ -26,5 +24,5 @@ int main(int argc, char** argv)
|
|||
myclass<int> y(1);
|
||||
//x = y;
|
||||
x += 1;
|
||||
assert(x == y);
|
||||
__CPROVER_assert(x == y, "");
|
||||
}
|
||||
|
|
|
@ -1,5 +1,3 @@
|
|||
#include <cassert>
|
||||
|
||||
template<class T>
|
||||
class myclass2;
|
||||
|
||||
|
@ -38,6 +36,6 @@ int main(int argc, char** argv)
|
|||
myclass2<int> x(0);
|
||||
myclass<int> y(1);
|
||||
x = y;
|
||||
assert(x == y);
|
||||
__CPROVER_assert(x == y, "");
|
||||
return 0;
|
||||
}
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
KNOWNBUG
|
||||
CORE
|
||||
main.cpp
|
||||
|
||||
^EXIT=0$
|
||||
|
|
|
@ -1,5 +1,3 @@
|
|||
#include <cassert>
|
||||
|
||||
template<class T>
|
||||
T inc(T x)
|
||||
{
|
||||
|
@ -15,5 +13,5 @@ int main(int argc, char** argv)
|
|||
x = inc<int>(x);
|
||||
y = inc<unsigned char>(y);
|
||||
|
||||
assert(x == y);
|
||||
__CPROVER_assert(x == y, "");
|
||||
}
|
||||
|
|
|
@ -1,6 +1,6 @@
|
|||
KNOWNBUG
|
||||
main.cpp
|
||||
|
||||
--object-bits 10
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
^VERIFICATION SUCCESSFUL$
|
||||
|
|
|
@ -1,5 +1,3 @@
|
|||
#include <cassert>
|
||||
|
||||
template <int W>
|
||||
class sc_uint {
|
||||
public:
|
||||
|
@ -54,7 +52,7 @@ int main(int argc, char** argv)
|
|||
z += y;
|
||||
|
||||
sc_uint<10> w(3);
|
||||
assert(z == w);
|
||||
__CPROVER_assert(z == w, "");
|
||||
|
||||
return 0;
|
||||
}
|
||||
|
|
|
@ -1,5 +1,3 @@
|
|||
#include <cassert>
|
||||
|
||||
#define DEF_INSIDE
|
||||
|
||||
template<class T>
|
||||
|
@ -35,8 +33,8 @@ int main (int argc, char *argv[])
|
|||
my_template<int> x;
|
||||
x.set(5);
|
||||
int y = x.get();
|
||||
assert(y==5);
|
||||
assert(z.get()==3);
|
||||
__CPROVER_assert(y == 5, "");
|
||||
__CPROVER_assert(z.get() == 3, "");
|
||||
|
||||
return 0;
|
||||
}
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
KNOWNBUG
|
||||
CORE
|
||||
main.cpp
|
||||
-DNO_IO -DNO_STRING
|
||||
^EXIT=0$
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
KNOWNBUG
|
||||
CORE
|
||||
main.cpp
|
||||
-DNO_IO -DNO_STRING
|
||||
^EXIT=0$
|
||||
|
|
|
@ -64,11 +64,22 @@ symbolt &cpp_declarator_convertert::convert(
|
|||
cpp_typecheck_resolve.resolve_scope(
|
||||
declarator.name(), base_name, template_args);
|
||||
|
||||
cpp_scopet *friend_scope = nullptr;
|
||||
|
||||
if(is_friend)
|
||||
{
|
||||
friend_scope = &cpp_typecheck.cpp_scopes.current_scope();
|
||||
save_scope.restore();
|
||||
}
|
||||
|
||||
scope=&cpp_typecheck.cpp_scopes.current_scope();
|
||||
|
||||
// check the declarator-part of the type, in that scope
|
||||
// check the declarator-part of the type, in the current scope
|
||||
if(declarator.value().is_nil() || !cpp_typecheck.has_auto(final_type))
|
||||
cpp_typecheck.typecheck_type(final_type);
|
||||
|
||||
if(friend_scope)
|
||||
scope = friend_scope;
|
||||
}
|
||||
|
||||
is_code=is_code_type(final_type);
|
||||
|
@ -80,9 +91,9 @@ symbolt &cpp_declarator_convertert::convert(
|
|||
get_final_identifier();
|
||||
|
||||
// first see if it is a member
|
||||
if(scope->id_class==cpp_idt::id_classt::CLASS && !is_friend)
|
||||
if(scope->id_class == cpp_idt::id_classt::CLASS)
|
||||
{
|
||||
// it's a member! it must be declared already
|
||||
// it's a member! it must be declared already, unless it's a friend
|
||||
|
||||
typet &method_qualifier=
|
||||
static_cast<typet &>(declarator.method_qualifier());
|
||||
|
@ -118,7 +129,15 @@ symbolt &cpp_declarator_convertert::convert(
|
|||
|
||||
// try again
|
||||
maybe_symbol=cpp_typecheck.symbol_table.get_writeable(final_identifier);
|
||||
if(!maybe_symbol)
|
||||
if(!maybe_symbol && is_friend)
|
||||
{
|
||||
symbolt &friend_symbol =
|
||||
convert_new_symbol(storage_spec, member_spec, declarator);
|
||||
// mark it as weak so that the full declaration can replace the symbol
|
||||
friend_symbol.is_weak = true;
|
||||
return friend_symbol;
|
||||
}
|
||||
else if(!maybe_symbol)
|
||||
{
|
||||
cpp_typecheck.error().source_location=
|
||||
declarator.name().source_location();
|
||||
|
@ -411,9 +430,7 @@ void cpp_declarator_convertert::get_final_identifier()
|
|||
}
|
||||
}
|
||||
|
||||
final_identifier=
|
||||
scope->prefix+
|
||||
identifier;
|
||||
final_identifier = scope->prefix + identifier;
|
||||
}
|
||||
|
||||
symbolt &cpp_declarator_convertert::convert_new_symbol(
|
||||
|
|
|
@ -48,7 +48,6 @@ cpp_idt &cpp_scopest::put_into_scope(
|
|||
{
|
||||
cpp_save_scopet saved_scope(*this);
|
||||
go_to(scope);
|
||||
go_to_global_scope();
|
||||
|
||||
cpp_idt &id=current_scope().insert(symbol.base_name);
|
||||
id.identifier=symbol.name;
|
||||
|
|
|
@ -861,13 +861,9 @@ void cpp_typecheckt::typecheck_friend_declaration(
|
|||
|
||||
if(declaration.is_template())
|
||||
{
|
||||
return; // TODO
|
||||
|
||||
#if 0
|
||||
error().source_location=declaration.type().source_location();
|
||||
error() << "friend template not supported" << eom;
|
||||
throw 0;
|
||||
#endif
|
||||
}
|
||||
|
||||
// we distinguish these whether there is a declarator
|
||||
|
@ -890,11 +886,10 @@ void cpp_typecheckt::typecheck_friend_declaration(
|
|||
throw 0;
|
||||
}
|
||||
|
||||
// typecheck ftype
|
||||
|
||||
// TODO
|
||||
// typecheck_type(ftype);
|
||||
// symbol.type.add("ID_C_friends").move_to_sub(ftype);
|
||||
cpp_save_scopet saved_scope(cpp_scopes);
|
||||
cpp_scopes.go_to_global_scope();
|
||||
typecheck_type(ftype);
|
||||
symbol.type.add(ID_C_friends).move_to_sub(ftype);
|
||||
|
||||
return;
|
||||
}
|
||||
|
@ -902,39 +897,30 @@ void cpp_typecheckt::typecheck_friend_declaration(
|
|||
// It should be a friend function.
|
||||
// Do the declarators.
|
||||
|
||||
#ifdef DEBUG
|
||||
std::cout << "friend declaration: " << declaration.pretty() << '\n';
|
||||
#endif
|
||||
|
||||
for(auto &sub_it : declaration.declarators())
|
||||
{
|
||||
bool has_value = sub_it.value().is_not_nil();
|
||||
|
||||
if(!has_value)
|
||||
{
|
||||
// If no value is found, then we jump to the
|
||||
// global scope, and we convert the declarator
|
||||
// as if it were declared there
|
||||
cpp_save_scopet saved_scope(cpp_scopes);
|
||||
cpp_scopes.go_to_global_scope();
|
||||
cpp_declarator_convertert cpp_declarator_converter(*this);
|
||||
const symbolt &conv_symb=cpp_declarator_converter.convert(
|
||||
declaration.type(), declaration.storage_spec(),
|
||||
declaration.member_spec(), sub_it);
|
||||
exprt symb_expr=cpp_symbol_expr(conv_symb);
|
||||
symbol.type.add(ID_C_friends).move_to_sub(symb_expr);
|
||||
}
|
||||
else
|
||||
{
|
||||
cpp_declarator_convertert cpp_declarator_converter(*this);
|
||||
cpp_declarator_converter.is_friend=true;
|
||||
#ifdef DEBUG
|
||||
std::cout << "decl: " << sub_it.pretty() << "\n with value "
|
||||
<< sub_it.value().pretty() << '\n';
|
||||
std::cout << " scope: " << cpp_scopes.current_scope().prefix << '\n';
|
||||
#endif
|
||||
|
||||
if(sub_it.value().is_not_nil())
|
||||
declaration.member_spec().set_inline(true);
|
||||
|
||||
const symbolt &conv_symb=cpp_declarator_converter.convert(
|
||||
declaration.type(), declaration.storage_spec(),
|
||||
declaration.member_spec(), sub_it);
|
||||
|
||||
exprt symb_expr=cpp_symbol_expr(conv_symb);
|
||||
|
||||
symbol.type.add(ID_C_friends).move_to_sub(symb_expr);
|
||||
}
|
||||
cpp_declarator_convertert cpp_declarator_converter(*this);
|
||||
cpp_declarator_converter.is_friend = true;
|
||||
const symbolt &conv_symb = cpp_declarator_converter.convert(
|
||||
declaration.type(),
|
||||
declaration.storage_spec(),
|
||||
declaration.member_spec(),
|
||||
sub_it);
|
||||
exprt symb_expr = cpp_symbol_expr(conv_symb);
|
||||
symbol.type.add(ID_C_friends).move_to_sub(symb_expr);
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -1322,7 +1308,13 @@ void cpp_typecheckt::typecheck_member_function(
|
|||
// move early, it must be visible before doing any value
|
||||
symbolt *new_symbol;
|
||||
|
||||
if(symbol_table.move(symbol, new_symbol))
|
||||
const bool symbol_exists = symbol_table.move(symbol, new_symbol);
|
||||
if(symbol_exists && new_symbol->is_weak)
|
||||
{
|
||||
// there might have been an earlier friend declaration
|
||||
*new_symbol = std::move(symbol);
|
||||
}
|
||||
else if(symbol_exists)
|
||||
{
|
||||
error().source_location=symbol.location;
|
||||
error() << "failed to insert new method symbol: " << symbol.name << '\n'
|
||||
|
|
|
@ -1251,10 +1251,21 @@ bool cpp_typecheckt::reference_binding(
|
|||
return false;
|
||||
}
|
||||
|
||||
if(expr.get_bool(ID_C_lvalue))
|
||||
if(expr.get_bool(ID_C_lvalue) || type.subtype().get_bool(ID_C_constant))
|
||||
{
|
||||
if(reference_compatible(expr, type, rank))
|
||||
{
|
||||
if(!expr.get_bool(ID_C_lvalue))
|
||||
{
|
||||
// create temporary object
|
||||
side_effect_exprt tmp{ID_temporary_object,
|
||||
{std::move(expr)},
|
||||
type.subtype(),
|
||||
expr.source_location()};
|
||||
tmp.set(ID_mode, ID_cpp);
|
||||
expr.swap(tmp);
|
||||
}
|
||||
|
||||
{
|
||||
address_of_exprt tmp(expr, reference_type(expr.type()));
|
||||
tmp.add_source_location()=expr.source_location();
|
||||
|
|
|
@ -1175,11 +1175,9 @@ void cpp_typecheckt::typecheck_expr_member(
|
|||
if(pcomp.is_nil())
|
||||
{
|
||||
error().source_location=expr.find_source_location();
|
||||
error() << "error: `"
|
||||
<< symbol_expr.get(ID_identifier)
|
||||
error() << "error: `" << symbol_expr.get(ID_identifier)
|
||||
<< "' is not static member "
|
||||
<< "of class `" << to_string(type) << "'"
|
||||
<< eom;
|
||||
<< "of class `" << to_string(op0.type()) << "'" << eom;
|
||||
throw 0;
|
||||
}
|
||||
}
|
||||
|
|
Loading…
Reference in New Issue