{

if(type.id()==ID_const)

return true;

else if(type.id()==ID_merged_type)

{

for(const typet &subtype : to_type_with_subtypes(type).subtypes())

{

if(has_const(subtype))

return true;

}

return false;

}

else

return false;

{

if(type.id()==ID_volatile)

return true;

else if(type.id()==ID_merged_type)

{

for(const typet &subtype : to_type_with_subtypes(type).subtypes())

{

if(has_volatile(subtype))

return true;

}

return false;

}

else

return false;

{

if(type.id() == ID_auto)

return true;

else if(

type.id() == ID_merged_type || type.id() == ID_frontend_pointer ||

type.id() == ID_pointer)

{

for(const typet &subtype : to_type_with_subtypes(type).subtypes())

{

if(has_auto(subtype))

return true;

}

return false;

}

else

return false;

struct_union_typet &type)

{

// first save qualifiers

c_qualifierst qualifiers(type);

// now clear them from the type

type.remove(ID_C_constant);

type.remove(ID_C_volatile);

type.remove(ID_C_restricted);

// get the tag name

bool has_tag=type.find(ID_tag).is_not_nil();

irep_idt base_name;

cpp_scopet *dest_scope=nullptr;

bool has_body=type.find(ID_body).is_not_nil();

bool tag_only_declaration=type.get_bool(ID_C_tag_only_declaration);

bool is_union = type.id() == ID_union;

if(!has_tag)

{

// most of these should be named by now; see

// cpp_declarationt::name_anon_struct_union()

base_name=std::string("#anon_")+std::to_string(++anon_counter);

type.set(ID_C_is_anonymous, true);

dest_scope=&cpp_scopes.current_scope();

}

else

{

const cpp_namet &cpp_name=

to_cpp_name(type.find(ID_tag));

// scope given?

if(cpp_name.is_simple_name())

{

base_name=cpp_name.get_base_name();

// anonymous structs always go into the current scope

if(type.get_bool(ID_C_is_anonymous))

dest_scope=&cpp_scopes.current_scope();

else

dest_scope=&tag_scope(base_name, has_body, tag_only_declaration);

}

else

{

cpp_save_scopet cpp_save_scope(cpp_scopes);

cpp_typecheck_resolvet cpp_typecheck_resolve(*this);

cpp_template_args_non_tct t_args;

dest_scope=

&cpp_typecheck_resolve.resolve_scope(cpp_name, base_name, t_args);

}

}

// The identifier 'tag-X' matches what the C front-end does!

// The hyphen is deliberate to avoid collisions with other

// identifiers.

const irep_idt symbol_name=

dest_scope->prefix+

"tag-"+id2string(base_name)+

dest_scope->suffix;

// check if we have it already

if(const auto maybe_symbol=symbol_table.lookup(symbol_name))

{

// we do!

const symbolt &symbol=*maybe_symbol;

if(has_body)

{

if(

symbol.type.id() == type.id() &&

to_struct_union_type(symbol.type).is_incomplete())

{

// a previously incomplete struct/union becomes complete

symbolt &writeable_symbol = symbol_table.get_writeable_ref(symbol_name);

writeable_symbol.type.swap(type);

typecheck_compound_body(writeable_symbol);

}

else if(symbol.type.get_bool(ID_C_is_anonymous))

{

// we silently ignore

}

else

{

error().source_location=type.source_location();

error() << "compound tag '" << base_name << "' declared previously\n"

<< "location of previous definition: " << symbol.location

<< eom;

throw 0;

}

}

else if(symbol.type.id() != type.id())

{

error().source_location = type.source_location();

error() << "redefinition of '" << symbol.pretty_name << "'"

<< " as different kind of tag" << eom;

throw 0;

}

}

else

{

// produce new symbol

type_symbolt symbol{symbol_name, type, ID_cpp};

symbol.base_name=base_name;

symbol.location=type.source_location();

symbol.module=module;

symbol.pretty_name=

cpp_scopes.current_scope().prefix+

id2string(symbol.base_name)+

cpp_scopes.current_scope().suffix;

symbol.type.set(

ID_tag, cpp_scopes.current_scope().prefix+id2string(symbol.base_name));

// move early, must be visible before doing body

symbolt *new_symbol;

if(symbol_table.move(symbol, new_symbol))

{

error().source_location=symbol.location;

error() << "cpp_typecheckt::typecheck_compound_type: "

<< "symbol_table.move() failed" << eom;

throw 0;

}

// put into dest_scope

cpp_idt &id=cpp_scopes.put_into_scope(*new_symbol, *dest_scope);

id.id_class=cpp_idt::id_classt::CLASS;

id.is_scope=true;

id.prefix=cpp_scopes.current_scope().prefix+

id2string(new_symbol->base_name)+

cpp_scopes.current_scope().suffix+"::";

id.class_identifier=new_symbol->name;

id.id_class=cpp_idt::id_classt::CLASS;

if(has_body)

typecheck_compound_body(*new_symbol);

else

{

struct_union_typet new_type(new_symbol->type.id());

new_type.set(ID_tag, new_symbol->base_name);

new_type.make_incomplete();

new_type.add_source_location() = type.source_location();

new_symbol->type.swap(new_type);

}

}

if(is_union)

{

// create union tag

union_tag_typet tag_type(symbol_name);

qualifiers.write(tag_type);

type.swap(tag_type);

}

else

{

// create struct tag

struct_tag_typet tag_type(symbol_name);

qualifiers.write(tag_type);

type.swap(tag_type);

}

const symbolt &symbol,

const cpp_declarationt &declaration,

cpp_declaratort &declarator,

struct_typet::componentst &components,

const irep_idt &access,

bool is_static,

bool is_typedef,

bool is_mutable)

{

bool is_cast_operator=

declaration.type().id()=="cpp-cast-operator";

if(is_cast_operator)

{

PRECONDITION(

declarator.name().get_sub().size() == 2 &&

declarator.name().get_sub().front().id() == ID_operator);

typet type=static_cast<typet &>(declarator.name().get_sub()[1]);

declarator.type().add_subtype() = type;

cpp_namet::namet name("(" + cpp_type2name(type) + ")");

declarator.name().get_sub().back().swap(name);

}

typet final_type=

declarator.merge_type(declaration.type());

// this triggers template elaboration

elaborate_class_template(final_type);

typecheck_type(final_type);

if(final_type.id() == ID_empty)

{

error().source_location = declaration.type().source_location();

error() << "void-typed member not permitted" << eom;

throw 0;

}

cpp_namet cpp_name;

cpp_name.swap(declarator.name());

irep_idt base_name;

if(cpp_name.is_nil())

{

// Yes, there can be members without name.

base_name=irep_idt();

}

else if(cpp_name.is_simple_name())

{

base_name=cpp_name.get_base_name();

}

else

{

error().source_location=cpp_name.source_location();

error() << "declarator in compound needs to be simple name"

<< eom;

throw 0;

}

bool is_method=!is_typedef && final_type.id()==ID_code;

bool is_constructor=declaration.is_constructor();

bool is_destructor=declaration.is_destructor();

bool is_virtual=declaration.member_spec().is_virtual();

bool is_explicit=declaration.member_spec().is_explicit();

bool is_inline=declaration.member_spec().is_inline();

final_type.set(ID_C_member_name, symbol.name);

// first do some sanity checks

if(is_virtual && !is_method)

{

error().source_location=cpp_name.source_location();

error() << "only methods can be virtual" << eom;

throw 0;

}

if(is_inline && !is_method)

{

error().source_location=cpp_name.source_location();

error() << "only methods can be inlined" << eom;

throw 0;

}

if(is_virtual && is_static)

{

error().source_location=cpp_name.source_location();

error() << "static methods cannot be virtual" << eom;

throw 0;

}

if(is_cast_operator && is_static)

{

error().source_location=cpp_name.source_location();

error() << "cast operators cannot be static" << eom;

throw 0;

}

if(is_constructor && is_virtual)

{

error().source_location=cpp_name.source_location();

error() << "constructors cannot be virtual" << eom;

throw 0;

}

if(!is_constructor && is_explicit)

{

error().source_location=cpp_name.source_location();

error() << "only constructors can be explicit" << eom;

throw 0;

}

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;

throw 0;

}

if(is_destructor &&

base_name!="~"+id2string(symbol.base_name))

{

error().source_location=cpp_name.source_location();

error() << "destructor with wrong name" << eom;

throw 0;

}

// now do actual work

irep_idt identifier;

// the below is a temporary hack

// if(is_method || is_static)

if(id2string(cpp_scopes.current_scope().prefix).find("#anon")==

std::string::npos ||

is_method || is_static)

{

// Identifiers for methods include the scope prefix.

// Identifiers for static members include the scope prefix.

identifier=

cpp_scopes.current_scope().prefix+

id2string(base_name);

}

else

{

// otherwise, we keep them simple

identifier=base_name;

}

struct_typet::componentt component(identifier, final_type);

component.set(ID_access, access);

component.set_base_name(base_name);

component.set_pretty_name(base_name);

component.add_source_location()=cpp_name.source_location();

if(cpp_name.is_operator())

{

component.set(ID_is_operator, true);

component.type().set(ID_C_is_operator, true);

}

if(is_cast_operator)

component.set(ID_is_cast_operator, true);

if(declaration.member_spec().is_explicit())

component.set(ID_is_explicit, true);

// either blank, const, volatile, or const volatile

const typet &method_qualifier=

static_cast<const typet &>(declarator.add(ID_method_qualifier));

if(is_static)

{

component.set(ID_is_static, true);

component.type().set(ID_C_is_static, true);

}

if(is_typedef)

component.set(ID_is_type, true);

if(is_mutable)

component.set(ID_is_mutable, true);

exprt &value=declarator.value();

irept &initializers=declarator.member_initializers();

if(is_method)

{

if(

value.id() == ID_code &&

to_code(value).get_statement() == ID_cpp_delete)

{

value.make_nil();

component.set(ID_access, ID_noaccess);

}

component.set(ID_is_inline, declaration.member_spec().is_inline());

// the 'virtual' name of the function

std::string virtual_name = id2string(component.get_base_name()) +

id2string(function_identifier(component.type()));

if(has_const(method_qualifier))

virtual_name+="$const";

if(has_volatile(method_qualifier))

virtual_name += "$volatile";

if(to_code_type(component.type()).return_type().id() == ID_destructor)

virtual_name="@dtor";

// The method may be virtual implicitly.

std::set<irep_idt> virtual_bases;

for(const auto &comp : components)

{

if(comp.get_bool(ID_is_virtual))

{

if(comp.get(ID_virtual_name) == virtual_name)

{

is_virtual=true;

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

DATA_INVARIANT(

!code_type.parameters().empty(), "must have parameters");

const typet &pointer_type=code_type.parameters()[0].type();

DATA_INVARIANT(

pointer_type.id() == ID_pointer, "this must be pointer");

virtual_bases.insert(

to_pointer_type(pointer_type).base_type().get(ID_identifier));

}

}

}

if(!is_virtual)

{

typecheck_member_function(

symbol, component, initializers,

method_qualifier, value);

if(!value.is_nil() && !is_static)

{

error().source_location=cpp_name.source_location();

error() << "no initialization allowed here" << eom;

throw 0;

}

}

else // virtual

{

component.type().set(ID_C_is_virtual, true);

component.type().set(ID_C_virtual_name, virtual_name);

// Check if it is a pure virtual method

if(value.is_not_nil() && value.is_constant())

{

mp_integer i;

to_integer(to_constant_expr(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(ID_is_pure_virtual, true);

value.make_nil();

}

typecheck_member_function(

symbol,

component,

initializers,

method_qualifier,

value);

// get the virtual-table symbol type

irep_idt vt_name="virtual_table::"+id2string(symbol.name);

if(!symbol_table.has_symbol(vt_name))

{

// first time: create a virtual-table symbol type

type_symbolt vt_symb_type{vt_name, struct_typet(), ID_cpp};

vt_symb_type.base_name="virtual_table::"+id2string(symbol.base_name);

vt_symb_type.pretty_name=vt_symb_type.base_name;

vt_symb_type.module=module;

vt_symb_type.location=symbol.location;

vt_symb_type.type.set(ID_name, vt_symb_type.name);

const bool failed=!symbol_table.insert(std::move(vt_symb_type)).second;

CHECK_RETURN(!failed);

// add a virtual-table pointer

struct_typet::componentt compo(

id2string(symbol.name) + "::@vtable_pointer",

pointer_type(struct_tag_typet(vt_name)));

compo.set_base_name("@vtable_pointer");

compo.set_pretty_name(id2string(symbol.base_name) + "@vtable_pointer");

compo.set(ID_is_vtptr, true);

compo.set(ID_access, ID_public);

components.push_back(compo);

put_compound_into_scope(compo);

}

typet &vt=symbol_table.get_writeable_ref(vt_name).type;

INVARIANT(vt.id()==ID_struct, "Virtual tables must be stored as struct");

struct_typet &virtual_table=to_struct_type(vt);

component.set(ID_virtual_name, virtual_name);

component.set(ID_is_virtual, is_virtual);

// add an entry to the virtual table

struct_typet::componentt vt_entry(

id2string(vt_name) + "::" + virtual_name,

pointer_type(component.type()));

vt_entry.set_base_name(virtual_name);

vt_entry.set_pretty_name(virtual_name);

vt_entry.set(ID_access, ID_public);

vt_entry.add_source_location()=symbol.location;

virtual_table.components().push_back(vt_entry);

// take care of overloading

while(!virtual_bases.empty())

{

irep_idt virtual_base=*virtual_bases.begin();

// a new function that does 'late casting' of the 'this' parameter

symbolt func_symb{

id2string(component.get_name()) + "::" + id2string(virtual_base),

component.type(),

symbol.mode};

func_symb.base_name = component.get_base_name();

func_symb.pretty_name = component.get_base_name();

func_symb.module=module;

func_symb.location=component.source_location();

// change the type of the 'this' pointer

code_typet &code_type=to_code_type(func_symb.type);

code_typet::parametert &this_parameter = code_type.parameters().front();

to_pointer_type(this_parameter.type())

.base_type()

.set(ID_identifier, virtual_base);

// create symbols for the parameters

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

std::size_t i=0;

for(auto &arg : args)

{

irep_idt param_base_name = arg.get_base_name();

if(param_base_name.empty())

param_base_name = "arg" + std::to_string(i++);

symbolt arg_symb{

id2string(func_symb.name) + "::" + id2string(param_base_name),

arg.type(),

symbol.mode};

arg_symb.base_name = param_base_name;

arg_symb.pretty_name = param_base_name;

arg_symb.location=func_symb.location;

arg.set_identifier(arg_symb.name);

// add the parameter to the symbol table

const bool failed=!symbol_table.insert(std::move(arg_symb)).second;

CHECK_RETURN(!failed);

}

// do the body of the function

typecast_exprt late_cast(

lookup(args[0].get_identifier()).symbol_expr(),

to_code_type(component.type()).parameters()[0].type());

side_effect_expr_function_callt expr_call(

symbol_exprt(component.get_name(), component.type()),

{late_cast},

uninitialized_typet{},

source_locationt{});

expr_call.arguments().reserve(args.size());

for(const auto &arg : args)

{

expr_call.arguments().push_back(

lookup(arg.get_identifier()).symbol_expr());

}

if(code_type.return_type().id()!=ID_empty &&

code_type.return_type().id()!=ID_destructor)

{

expr_call.type()=to_code_type(component.type()).return_type();

func_symb.value = code_blockt{{code_frontend_returnt(

already_typechecked_exprt{std::move(expr_call)})}};

}

else

{

func_symb.value = code_blockt{{code_expressiont(

already_typechecked_exprt{std::move(expr_call)})}};

}

// add this new function to the list of components

struct_typet::componentt new_compo=component;

new_compo.type()=func_symb.type;

new_compo.set_name(func_symb.name);

components.push_back(new_compo);

// add the function to the symbol table

{

const bool failed=!symbol_table.insert(std::move(func_symb)).second;

CHECK_RETURN(!failed);

}

put_compound_into_scope(new_compo);

// next base

virtual_bases.erase(virtual_bases.begin());

}

}

}

if(is_static && !is_method) // static non-method member

{

// add as global variable to symbol_table

symbolt static_symbol{identifier, component.type(), symbol.mode};

static_symbol.base_name = component.get_base_name();

static_symbol.is_lvalue=true;

static_symbol.is_static_lifetime=true;

static_symbol.location=cpp_name.source_location();

static_symbol.is_extern=true;

// TODO: not sure about this: should be defined separately!

dynamic_initializations.push_back(static_symbol.name);

symbolt *new_symbol;

if(symbol_table.move(static_symbol, new_symbol))

{

error().source_location=cpp_name.source_location();

error() << "redeclaration of static member '" << static_symbol.base_name

<< "'" << eom;

throw 0;

}

if(value.is_not_nil())

{

if(cpp_is_pod(new_symbol->type))

{

new_symbol->value.swap(value);

c_typecheck_baset::do_initializer(*new_symbol);

}

else

{

symbol_exprt symexpr = symbol_exprt::typeless(new_symbol->name);

exprt::operandst ops;

ops.push_back(value);

auto defcode = cpp_constructor(source_locationt(), symexpr, ops);

CHECK_RETURN(defcode.has_value());

new_symbol->value.swap(defcode.value());

}

}

}

// array members must have fixed size

check_fixed_size_array(component.type());

put_compound_into_scope(component);

components.push_back(component);

{

if(type.id()==ID_array)

{

array_typet &array_type=to_array_type(type);

if(array_type.size().is_not_nil())

{

if(array_type.size().id() == ID_symbol)

{

const symbol_exprt &s = to_symbol_expr(array_type.size());

const symbolt &symbol = lookup(s.identifier());

if(cpp_is_pod(symbol.type) && symbol.type.get_bool(ID_C_constant))

array_type.size() = symbol.value;

}

make_constant_index(array_type.size());

}

// recursive call for multi-dimensional arrays

check_fixed_size_array(array_type.element_type());

}

const struct_union_typet::componentt &compound)

{

const irep_idt &base_name=compound.get_base_name();

const irep_idt &name=compound.get_name();

// nothing to do if no base_name (e.g., an anonymous bitfield)

if(base_name.empty())

return;

if(compound.type().id()==ID_code)

{

// put the symbol into scope

cpp_idt &id=cpp_scopes.current_scope().insert(base_name);

id.id_class = compound.get_bool(ID_is_type) ? cpp_idt::id_classt::TYPEDEF

: cpp_idt::id_classt::SYMBOL;

id.identifier=name;

id.class_identifier=cpp_scopes.current_scope().identifier;

id.is_member=true;

id.is_constructor =

to_code_type(compound.type()).return_type().id() == ID_constructor;

id.is_method=true;

id.is_static_member=compound.get_bool(ID_is_static);

// create function block-scope in the scope

cpp_idt &id_block=

cpp_scopes.current_scope().insert(

irep_idt(std::string("$block:") + base_name.c_str()));

id_block.id_class=cpp_idt::id_classt::BLOCK_SCOPE;

id_block.identifier=name;

id_block.class_identifier=cpp_scopes.current_scope().identifier;

id_block.is_method=true;

id_block.is_static_member=compound.get_bool(ID_is_static);

id_block.is_scope=true;

id_block.prefix = compound.get_string(ID_prefix);

cpp_scopes.id_map[id.identifier]=&id_block;

}

else

{

// check if it's already there

const auto id_set =

cpp_scopes.current_scope().lookup(base_name, cpp_scopet::SCOPE_ONLY);

for(const auto &id_it : id_set)

{

const cpp_idt &id=*id_it;

// the name is already in the scope

// this is ok if they belong to different categories

if(!id.is_class() && !id.is_enum())

{

error().source_location=compound.source_location();

error() << "'" << base_name << "' already in compound scope" << eom;

throw 0;

}

}

// put into the scope

cpp_idt &id=cpp_scopes.current_scope().insert(base_name);

id.id_class=compound.get_bool(ID_is_type)?

cpp_idt::id_classt::TYPEDEF:

cpp_idt::id_classt::SYMBOL;

id.identifier=name;

id.class_identifier=cpp_scopes.current_scope().identifier;

id.is_member=true;

id.is_method=false;

id.is_static_member=compound.get_bool(ID_is_static);

}

symbolt &symbol,

cpp_declarationt &declaration)

{

// A friend of a class can be a function/method,

// or a struct/class/union type.

if(declaration.is_template())

{

error().source_location=declaration.type().source_location();

error() << "friend template not supported" << eom;

throw 0;

}

// we distinguish these whether there is a declarator

if(declaration.declarators().empty())

{

typet &ftype=declaration.type();

// must be struct or union

if(ftype.id()!=ID_struct && ftype.id()!=ID_union)

{

error().source_location=declaration.type().source_location();

error() << "unexpected friend" << eom;

throw 0;

}

if(ftype.find(ID_body).is_not_nil())

{

error().source_location=declaration.type().source_location();

error() << "friend declaration must not have compound body" << eom;

throw 0;

}

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;

}

// 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())

{

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

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

}

{

cpp_save_scopet saved_scope(cpp_scopes);

// enter scope of compound

cpp_scopes.set_scope(symbol.name);

PRECONDITION(symbol.type.id() == ID_struct || symbol.type.id() == ID_union);

struct_union_typet &type=

to_struct_union_type(symbol.type);

// pull the base types in

if(!type.find(ID_bases).get_sub().empty())

{

if(type.id()==ID_union)

{

error().source_location=symbol.location;

error() << "union types must not have bases" << eom;

throw 0;

}

typecheck_compound_bases(to_struct_type(type));

}

exprt &body=static_cast<exprt &>(type.add(ID_body));

struct_union_typet::componentst &components=type.components();

symbol.type.set(ID_name, symbol.name);

// default access

irep_idt access = type.default_access();

bool found_ctor=false;

bool found_dtor=false;

// we first do everything _but_ the constructors

Forall_operands(it, body)

{

if(it->id()==ID_cpp_declaration)

{

cpp_declarationt &declaration=

to_cpp_declaration(*it);

if(declaration.member_spec().is_friend())

{

typecheck_friend_declaration(symbol, declaration);

continue; // done

}

if(declaration.is_template())

{

// remember access mode

declaration.set(ID_C_access, access);

convert_template_declaration(declaration);

continue;

}

if(declaration.type().id().empty())

continue;

bool is_typedef=declaration.is_typedef();

// is it tag-only?

if(declaration.type().id()==ID_struct ||