const source_locationt &source_location,

const irep_idt &parent_base_name,

const irep_idt &arg_name,

exprt &block)

{

exprt op0(

"explicit-typecast",

pointer_type(cpp_namet(parent_base_name, source_location).as_type()));

op0.copy_to_operands(exprt("cpp-this"));

op0.add_source_location()=source_location;

exprt op1(

"explicit-typecast",

pointer_type(cpp_namet(parent_base_name, source_location).as_type()));

op1.type().set(ID_C_reference, true);

to_pointer_type(op1.type()).base_type().set(ID_C_constant, true);

op1.get_sub().push_back(cpp_namet(arg_name, source_location));

op1.add_source_location()=source_location;

code_frontend_assignt code(dereference_exprt(op0), op1);

code.add_source_location() = source_location;

block.operands().push_back(code);

const source_locationt &source_location,

const irep_idt &member_base_name,

const irep_idt &arg_name,

exprt &block)

{

cpp_namet op0(member_base_name, source_location);

exprt op1(ID_member);

op1.add(ID_component_cpp_name, cpp_namet(member_base_name, source_location));

op1.copy_to_operands(cpp_namet(arg_name, source_location).as_expr());

op1.add_source_location()=source_location;

side_effect_expr_assignt assign(op0.as_expr(), op1, typet(), source_location);

assign.lhs().add_source_location() = source_location;

code_expressiont code(assign);

code.add_source_location() = source_location;

block.operands().push_back(code);

const source_locationt &source_location,

const irep_idt &member_base_name,

mp_integer i,

const irep_idt &arg_name,

exprt &block)

{

// Build the index expression

const exprt constant = from_integer(i, c_index_type());

const cpp_namet array(member_base_name, source_location);

exprt member(ID_member);

member.add(

ID_component_cpp_name, cpp_namet(member_base_name, source_location));

member.copy_to_operands(cpp_namet(arg_name, source_location).as_expr());

side_effect_expr_assignt assign(

index_exprt(array.as_expr(), constant),

index_exprt(member, constant),

typet(),

source_location);

assign.lhs().add_source_location() = source_location;

assign.rhs().add_source_location() = source_location;

code_expressiont code(assign);

code.add_source_location() = source_location;

block.operands().push_back(code);

const source_locationt &source_location,

const irep_idt &base_name,

cpp_declarationt &ctor) const

{

cpp_declaratort decl;

decl.name() = cpp_namet(base_name, source_location);

decl.type()=typet(ID_function_type);

decl.type().add_subtype().make_nil();

decl.add_source_location()=source_location;

decl.value() = code_blockt();

decl.add(ID_cv).make_nil();

decl.add(ID_throw_decl).make_nil();

ctor.type().id(ID_constructor);

ctor.add(ID_storage_spec).id(ID_cpp_storage_spec);

ctor.add_to_operands(std::move(decl));

ctor.add_source_location()=source_location;

const symbolt &symbol,

cpp_declarationt &cpctor) const

{

source_locationt source_location=symbol.type.source_location();

source_location.set_function(

id2string(symbol.base_name)+

"::"+id2string(symbol.base_name)+

"(const "+id2string(symbol.base_name)+" &)");

// Produce default constructor first

default_ctor(source_location, symbol.base_name, cpctor);

cpp_declaratort &decl0=cpctor.declarators()[0];

std::string param_identifier("ref");

// Compound name

const cpp_namet cppcomp(symbol.base_name, source_location);

// Parameter name

const cpp_namet cpp_parameter(param_identifier, source_location);

// Parameter declarator

cpp_declaratort parameter_tor;

parameter_tor.add(ID_value).make_nil();

parameter_tor.set(ID_name, cpp_parameter);

parameter_tor.type() = reference_type(uninitialized_typet{});

parameter_tor.add_source_location()=source_location;

// Parameter declaration

cpp_declarationt parameter_decl;

parameter_decl.set(ID_type, ID_merged_type);

auto &sub = to_type_with_subtypes(parameter_decl.type()).subtypes();

sub.push_back(cppcomp.as_type());

irept constnd(ID_const);

sub.push_back(static_cast<const typet &>(constnd));

parameter_decl.add_to_operands(std::move(parameter_tor));

parameter_decl.add_source_location()=source_location;

// Add parameter to function type

decl0.add(ID_type).add(ID_parameters).get_sub().push_back(parameter_decl);

decl0.add_source_location()=source_location;

irept &initializers=decl0.add(ID_member_initializers);

initializers.id(ID_member_initializers);

cpp_declaratort &declarator =

static_cast<cpp_declaratort &>(to_multi_ary_expr(cpctor).op0());

exprt &block=declarator.value();

// First, we need to call the parent copy constructors

for(const auto &b : to_struct_type(symbol.type).bases())

{

DATA_INVARIANT(b.id() == ID_base, "base class expression expected");

const symbolt &parsymb = lookup(b.type());

if(cpp_is_pod(parsymb.type))

copy_parent(source_location, parsymb.base_name, param_identifier, block);

else

{

irep_idt ctor_name=parsymb.base_name;

// Call the parent default copy constructor

const cpp_namet cppname(ctor_name, source_location);

codet mem_init(ID_member_initializer);

mem_init.add_source_location()=source_location;

mem_init.set(ID_member, cppname);

mem_init.copy_to_operands(cpp_parameter.as_expr());

initializers.move_to_sub(mem_init);

}

}

// Then, we add the member initializers

const struct_typet::componentst &components=

to_struct_type(symbol.type).components();

for(const auto &mem_c : components)

{

// Take care of virtual tables

if(mem_c.get_bool(ID_is_vtptr))

{

const cpp_namet cppname(mem_c.get_base_name(), source_location);

const symbolt &virtual_table_symbol_type =

lookup(to_pointer_type(mem_c.type()).base_type().get(ID_identifier));

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);

CHECK_RETURN(address.type() == mem_c.type());

already_typechecked_exprt::make_already_typechecked(address);

exprt ptrmember(ID_ptrmember);

ptrmember.set(ID_component_name, mem_c.get_name());

ptrmember.operands().push_back(exprt("cpp-this"));

code_frontend_assignt assign(ptrmember, address);

initializers.move_to_sub(assign);

continue;

}

if(

mem_c.get_bool(ID_from_base) || mem_c.get_bool(ID_is_type) ||

mem_c.get_bool(ID_is_static) || mem_c.type().id() == ID_code)

{

continue;

}

const irep_idt &mem_name = mem_c.get_base_name();

const cpp_namet cppname(mem_name, source_location);

codet mem_init(ID_member_initializer);

mem_init.set(ID_member, cppname);

mem_init.add_source_location()=source_location;

exprt memberexpr(ID_member);

memberexpr.set(ID_component_cpp_name, cppname);

memberexpr.copy_to_operands(cpp_parameter.as_expr());

memberexpr.add_source_location()=source_location;

if(mem_c.type().id() == ID_array)

memberexpr.set(ID_C_array_ini, true);

mem_init.add_to_operands(std::move(memberexpr));

initializers.move_to_sub(mem_init);

}

const symbolt &symbol,

cpp_declarationt &cpctor)

{

source_locationt source_location=symbol.type.source_location();

source_location.set_function(

id2string(symbol.base_name)

+ "& "+

id2string(symbol.base_name)+

"::operator=( const "+id2string(symbol.base_name)+"&)");

std::string arg_name("ref");

cpctor.add(ID_storage_spec).id(ID_cpp_storage_spec);

cpctor.type().id(ID_struct_tag);

cpctor.type().add(ID_identifier).id(symbol.name);

cpctor.operands().push_back(exprt(ID_cpp_declarator));

cpctor.add_source_location()=source_location;

cpp_declaratort &declarator =

static_cast<cpp_declaratort &>(to_multi_ary_expr(cpctor).op0());

declarator.add_source_location()=source_location;

cpp_namet &declarator_name=declarator.name();

typet &declarator_type=declarator.type();

declarator_type.add_source_location()=source_location;

declarator_name.id(ID_cpp_name);

declarator_name.get_sub().push_back(irept(ID_operator));

declarator_name.get_sub().push_back(irept("="));

declarator_type.id(ID_function_type);

declarator_type.add_subtype() = reference_type(uninitialized_typet{});

to_type_with_subtype(declarator_type)

.subtype()

.add(ID_C_qualifier)

.make_nil();

exprt &args=static_cast<exprt&>(declarator.type().add(ID_parameters));

args.add_source_location()=source_location;

args.get_sub().push_back(irept(ID_cpp_declaration));

cpp_declarationt &args_decl=

static_cast<cpp_declarationt&>(args.get_sub().back());

auto &args_decl_type_sub = to_type_with_subtypes(args_decl.type()).subtypes();

args_decl.type().id(ID_merged_type);

args_decl_type_sub.push_back(

cpp_namet(symbol.base_name, source_location).as_type());

args_decl_type_sub.push_back(typet(ID_const));

args_decl.operands().push_back(exprt(ID_cpp_declarator));

args_decl.add_source_location()=source_location;

cpp_declaratort &args_decl_declor=

static_cast<cpp_declaratort&>(args_decl.operands().back());

args_decl_declor.name() = cpp_namet(arg_name, source_location);

args_decl_declor.add_source_location()=source_location;

args_decl_declor.type() = pointer_type(uninitialized_typet{});

args_decl_declor.type().set(ID_C_reference, true);

args_decl_declor.value().make_nil();

const symbolt &symbol,

cpp_declaratort &declarator)

{

// save source location

source_locationt source_location=declarator.source_location();

declarator.make_nil();

code_blockt block;

std::string arg_name("ref");

// First, we copy the parents

for(const auto &b : to_struct_type(symbol.type).bases())

{

DATA_INVARIANT(b.id() == ID_base, "base class expression expected");

const symbolt &symb = lookup(b.type());

copy_parent(source_location, symb.base_name, arg_name, block);

}

// Then, we copy the members

for(const auto &c : to_struct_type(symbol.type).components())

{

if(

c.get_bool(ID_from_base) || c.get_bool(ID_is_type) ||

c.get_bool(ID_is_static) || c.get_bool(ID_is_vtptr) ||

c.type().id() == ID_code)

{

continue;

}

const irep_idt &mem_name = c.get_base_name();

if(c.type().id() == ID_array)

{

const exprt &size_expr = to_array_type(c.type()).size();

if(size_expr.id()==ID_infinity)

{

// error().source_location=object);

// err << "cannot copy array of infinite size\n";

// throw 0;

continue;

}

const auto size = numeric_cast<mp_integer>(size_expr);

CHECK_RETURN(!size.has_value());

CHECK_RETURN(*size >= 0);

for(mp_integer i = 0; i < *size; ++i)

copy_array(source_location, mem_name, i, arg_name, block);

}

else

copy_member(source_location, mem_name, arg_name, block);

}

// Finally we add the return statement

block.add(

code_returnt(dereference_exprt(exprt("cpp-this"), uninitialized_typet())));

declarator.value() = std::move(block);

declarator.value().add_source_location() = source_location;

const struct_typet::basest &bases,

const struct_typet::componentst &components,

const irept &initializers)

{

PRECONDITION(initializers.id() == ID_member_initializers);

for(const auto &initializer : initializers.get_sub())

{

PRECONDITION(initializer.is_not_nil());

const cpp_namet &member_name=

to_cpp_name(initializer.find(ID_member));

bool has_template_args=member_name.has_template_args();

if(has_template_args)

{

// it has to be a parent constructor

typet member_type=(typet&) initializer.find(ID_member);

typecheck_type(member_type);

// check for a direct parent

bool ok=false;

for(const auto &b : bases)

{

if(

to_struct_tag_type(member_type).get_identifier() ==

to_struct_tag_type(b.type()).get_identifier())

{

ok=true;

break;

}

}

if(!ok)

{

error().source_location=member_name.source_location();

error() << "invalid initializer '" << member_name.to_string() << "'"

<< eom;

throw 0;

}

return;

}

irep_idt base_name=member_name.get_base_name();

bool ok=false;

for(const auto &c : components)

{

if(c.get_base_name() != base_name)

continue;

// Data member

if(

!c.get_bool(ID_from_base) && !c.get_bool(ID_is_static) &&

c.type().id() != ID_code)

{

ok=true;

break;

}

// Maybe it is a parent constructor?

if(c.get_bool(ID_is_type))

{

if(c.type().id() != ID_struct_tag)

continue;

const symbolt &symb =

lookup(to_struct_tag_type(c.type()).get_identifier());

if(symb.type.id()!=ID_struct)

break;

// check for a direct parent

for(const auto &b : bases)

{

if(symb.name == to_struct_tag_type(b.type()).get_identifier())

{

ok=true;

break;

}

}

continue;

}

// Parent constructor

if(

c.get_bool(ID_from_base) && !c.get_bool(ID_is_type) &&

!c.get_bool(ID_is_static) && c.type().id() == ID_code &&

to_code_type(c.type()).return_type().id() == ID_constructor)

{

typet member_type=(typet&) initializer.find(ID_member);

typecheck_type(member_type);

// check for a direct parent

for(const auto &b : bases)

{

if(

member_type.get(ID_identifier) ==

to_struct_tag_type(b.type()).get_identifier())

{

ok=true;

break;

}

}

break;

}

}

if(!ok)

{

error().source_location=member_name.source_location();

error() << "invalid initializer '" << base_name << "'" << eom;

throw 0;

}

}

const struct_union_typet &struct_union_type,

irept &initializers)

{

const struct_union_typet::componentst &components=

struct_union_type.components();

PRECONDITION(initializers.id() == ID_member_initializers);

irept final_initializers(ID_member_initializers);

if(struct_union_type.id()==ID_struct)

{

// First, if we are the most-derived object, then

// we need to construct the virtual bases

std::list<irep_idt> vbases;

get_virtual_bases(to_struct_type(struct_union_type), vbases);

if(!vbases.empty())

{

code_blockt block;

while(!vbases.empty())

{

const symbolt &symb=lookup(vbases.front());

if(!cpp_is_pod(symb.type))

{

// default initializer

const cpp_namet cppname(symb.base_name);

codet mem_init(ID_member_initializer);

mem_init.set(ID_member, cppname);

block.move_to_sub(mem_init);

}

vbases.pop_front();

}

code_ifthenelset cond(

cpp_namet("@most_derived").as_expr(), std::move(block));

final_initializers.move_to_sub(cond);

}

// Subsequently, we need to call the non-POD parent constructors

for(const auto &b : to_struct_type(struct_union_type).bases())

{

DATA_INVARIANT(b.id() == ID_base, "base class expression expected");

const symbolt &ctorsymb = lookup(b.type());

if(cpp_is_pod(ctorsymb.type))

continue;

irep_idt ctor_name=ctorsymb.base_name;

// Check if the initialization list of the constructor

// explicitly calls the parent constructor.

bool found=false;

for(irept initializer : initializers.get_sub())

{

const cpp_namet &member_name=

to_cpp_name(initializer.find(ID_member));

bool has_template_args=member_name.has_template_args();

if(!has_template_args)

{

irep_idt base_name=member_name.get_base_name();

// check if the initializer is a data

bool is_data=false;

for(const auto &c : components)

{

if(

c.get_base_name() == base_name && c.type().id() != ID_code &&

!c.get_bool(ID_is_type))

{

is_data=true;

break;

}

}

if(is_data)

continue;

}

typet member_type=

static_cast<const typet&>(initializer.find(ID_member));

typecheck_type(member_type);

if(member_type.id() != ID_struct_tag)

break;

if(

to_struct_tag_type(b.type()).get_identifier() ==

to_struct_tag_type(member_type).get_identifier())

{

final_initializers.move_to_sub(initializer);

found=true;

break;

}

}

// Call the parent default constructor

if(!found)

{

const cpp_namet cppname(ctor_name);

codet mem_init(ID_member_initializer);

mem_init.set(ID_member, cppname);

final_initializers.move_to_sub(mem_init);

}

if(b.get_bool(ID_virtual))

{

codet tmp(ID_member_initializer);

tmp.swap(final_initializers.get_sub().back());

code_ifthenelset cond(

cpp_namet("@most_derived").as_expr(), std::move(tmp));

final_initializers.get_sub().back().swap(cond);

}

}

}

// Then, we add the member initializers

for(const auto &c : components)

{

// Take care of virtual tables

if(c.get_bool(ID_is_vtptr))

{

const cpp_namet cppname(c.get_base_name(), c.source_location());

const symbolt &virtual_table_symbol_type =

lookup(to_pointer_type(c.type()).base_type().get(ID_identifier));

const symbolt &virtual_table_symbol_var =

lookup(id2string(virtual_table_symbol_type.name) + "@" +

id2string(struct_union_type.get(ID_name)));

exprt var=virtual_table_symbol_var.symbol_expr();

address_of_exprt address(var);

CHECK_RETURN(address.type() == c.type());

already_typechecked_exprt::make_already_typechecked(address);

exprt ptrmember(ID_ptrmember);

ptrmember.set(ID_component_name, c.get_name());

ptrmember.operands().push_back(exprt("cpp-this"));

code_frontend_assignt assign(ptrmember, address);

final_initializers.move_to_sub(assign);

continue;

}

if(

c.get_bool(ID_from_base) || c.type().id() == ID_code ||

c.get_bool(ID_is_type) || c.get_bool(ID_is_static))

{

continue;

}

const irep_idt &mem_name = c.get_base_name();

// Check if the initialization list of the constructor

// explicitly initializes the data member

bool found=false;

for(auto &initializer : initializers.get_sub())

{

if(initializer.get(ID_member)!=ID_cpp_name)

continue;

cpp_namet &member_name=(cpp_namet&) initializer.add(ID_member);

if(member_name.has_template_args())

continue; // base-type initializer

irep_idt base_name=member_name.get_base_name();

if(mem_name==base_name)

{

final_initializers.move_to_sub(initializer);

found=true;

break;

}

}

// If the data member is a reference, it must be explicitly

// initialized

if(

!found && c.type().id() == ID_pointer &&

c.type().get_bool(ID_C_reference))

{

error().source_location = c.source_location();

error() << "reference must be explicitly initialized" << eom;

throw 0;

}

// If the data member is not POD and is not explicitly initialized,

// then its default constructor is called.

if(!found && !cpp_is_pod(c.type()))

{

cpp_namet cppname(mem_name);

codet mem_init(ID_member_initializer);

mem_init.set(ID_member, cppname);

final_initializers.move_to_sub(mem_init);

}

}

initializers.swap(final_initializers);

{

for(const auto &component : to_struct_type(symbol.type).components())

{

// Skip non-ctor

if(component.type().id()!=ID_code ||

to_code_type(component.type()).return_type().id() !=ID_constructor)

continue;

// Skip inherited constructor

if(component.get_bool(ID_from_base))

continue;

const code_typet &code_type=to_code_type(component.type());

const code_typet::parameterst &parameters=code_type.parameters();

// First parameter is the 'this' pointer. Therefore, copy

// constructors have at least two parameters

if(parameters.size() < 2)

continue;

const code_typet::parametert &parameter1=parameters[1];

const typet &parameter1_type=parameter1.type();

if(!is_reference(parameter1_type))

continue;

if(

to_reference_type(parameter1_type).base_type().get(ID_identifier) !=

symbol.name)

{

continue;

}

bool defargs=true;

for(std::size_t i=2; i<parameters.size(); i++)

{

if(parameters[i].default_value().is_nil())

{

defargs=false;

break;

}

}

if(defargs)

return true;

}

return false;

{

const struct_typet &struct_type=to_struct_type(symbol.type);

const struct_typet::componentst &components=struct_type.components();

for(const auto &component : components)

{

if(component.get_base_name() != "operator=")

continue;

if(component.get_bool(ID_is_static))

continue;

if(component.get_bool(ID_from_base))

continue;

const code_typet &code_type=to_code_type(component.type());

const code_typet::parameterst &args=code_type.parameters();

if(args.size()!=2)

continue;

const code_typet::parametert &arg1=args[1];

const typet &arg1_type=arg1.type();

if(!is_reference(arg1_type))

continue;

if(

to_reference_type(arg1_type).base_type().get(ID_identifier) !=

symbol.name)

continue;

return true;

}

return false;