{

const irep_idt &statement=code.get_statement();

if(statement==ID_try_catch)

{

code.type() = empty_typet();

typecheck_try_catch(code);

}

else if(statement==ID_member_initializer)

{

code.type() = empty_typet();

typecheck_member_initializer(code);

}

else if(statement==ID_msc_if_exists ||

statement==ID_msc_if_not_exists)

{

}

else if(statement==ID_decl_block)

{

// type checked already

}

else if(statement == ID_expression)

{

if(

!code.has_operands() || code.op0().id() != ID_side_effect ||

to_side_effect_expr(code.op0()).get_statement() != ID_assign)

{

c_typecheck_baset::typecheck_code(code);

return;

}

// as an extension, we support indexed access into signed/unsigned

// bitvectors, typically used with __CPROVER::(un)signedbv<N>

exprt &expr = code.op0();

if(expr.operands().size() == 2)

{

auto &binary_expr = to_binary_expr(expr);

if(binary_expr.op0().id() == ID_index)

{

exprt array = to_index_expr(binary_expr.op0()).array();

typecheck_expr(array);

if(

array.type().id() == ID_signedbv ||

array.type().id() == ID_unsignedbv)

{

shl_exprt shl{from_integer(1, array.type()),

to_index_expr(binary_expr.op0()).index()};

exprt rhs = if_exprt{

equal_exprt{

binary_expr.op1(), from_integer(0, binary_expr.op1().type())},

bitand_exprt{array, bitnot_exprt{shl}},

bitor_exprt{array, shl}};

binary_expr.op0() = to_index_expr(binary_expr.op0()).array();

binary_expr.op1() = rhs;

}

}

}

c_typecheck_baset::typecheck_code(code);

}

else

c_typecheck_baset::typecheck_code(code);

{

bool first = true;

for(auto &op : code.operands())

{

if(first)

{

// this is the 'try'

typecheck_code(to_code(op));

first = false;

}

else

{

// This is (one of) the catch clauses.

code_blockt &catch_block = to_code_block(to_code(op));

// look at the catch operand

auto &statements = catch_block.statements();

PRECONDITION(!statements.empty());

if(statements.front().get_statement() == ID_ellipsis)

{

statements.erase(statements.begin());

// do body

typecheck_code(catch_block);

}

else

{

// turn references into non-references

{

code_frontend_declt &decl = to_code_frontend_decl(statements.front());

cpp_declarationt &cpp_declaration = to_cpp_declaration(decl.symbol());

PRECONDITION(cpp_declaration.declarators().size() == 1);

cpp_declaratort &declarator=cpp_declaration.declarators().front();

if(is_reference(declarator.type()))

declarator.type() =

to_reference_type(declarator.type()).base_type();

}

// typecheck the body

typecheck_code(catch_block);

// the declaration is now in a decl_block

CHECK_RETURN(!catch_block.statements().empty());

CHECK_RETURN(

catch_block.statements().front().get_statement() == ID_decl_block);

// get the declaration

const code_frontend_declt &code_decl = to_code_frontend_decl(

to_code(catch_block.statements().front().op0()));

// get the type

const typet &type = code_decl.symbol().type();

// annotate exception ID

op.set(ID_exception_id, cpp_exception_id(type, *this));

}

}

}

{

// In addition to the C syntax, C++ also allows a declaration

// as condition. E.g.,

// if(void *p=...) ...

if(code.cond().id()==ID_code)

{

typecheck_code(to_code(code.cond()));

}

else

c_typecheck_baset::typecheck_ifthenelse(code);

{

// In addition to the C syntax, C++ also allows a declaration

// as condition. E.g.,

// while(void *p=...) ...

if(code.cond().id()==ID_code)

{

typecheck_code(to_code(code.cond()));

}

else

c_typecheck_baset::typecheck_while(code);

{

// In addition to the C syntax, C++ also allows a declaration

// as condition. E.g.,

// switch(int i=...) ...

exprt &value = to_code_switch(code).value();

if(value.id() == ID_code)

{

// we shall rewrite that into

// { int i=....; switch(i) .... }

codet decl = to_code(value);

typecheck_decl(decl);

CHECK_RETURN(decl.get_statement() == ID_decl_block);

CHECK_RETURN(decl.operands().size() == 1);

// replace declaration by its symbol

value = to_code_frontend_decl(to_code(to_unary_expr(decl).op())).symbol();

c_typecheck_baset::typecheck_switch(code);

code_blockt code_block({to_code(decl.op0()), code});

code.swap(code_block);

}

else

c_typecheck_baset::typecheck_switch(code);

{

const cpp_namet &member=

to_cpp_name(code.find(ID_member));

// Let's first typecheck the operands.

Forall_operands(it, code)

{

const bool has_array_ini = it->get_bool(ID_C_array_ini);

typecheck_expr(*it);

if(has_array_ini)

it->set(ID_C_array_ini, true);

}

// The initializer may be a data member (non-type)

// or a parent class (type).

// We ask for VAR only, as we get the parent classes via their

// constructor!

cpp_typecheck_fargst fargs;

fargs.in_use=true;

fargs.operands=code.operands();

// We should only really resolve in qualified mode,

// no need to look into the parent.

// Plus, this should happen in class scope, not the scope of

// the constructor because of the constructor arguments.

exprt symbol_expr=

resolve(member, cpp_typecheck_resolvet::wantt::VAR, fargs);

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

{

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

DATA_INVARIANT(

code_type.parameters().size() >= 1, "at least one parameter");

// It's a parent. Call the constructor that we got.

side_effect_expr_function_callt function_call(

symbol_expr, {}, uninitialized_typet{}, code.source_location());

function_call.arguments().reserve(code.operands().size()+1);

// we have to add 'this'

exprt this_expr = cpp_scopes.current_scope().this_expr;

PRECONDITION(this_expr.is_not_nil());

make_ptr_typecast(

this_expr, to_pointer_type(code_type.parameters().front().type()));

function_call.arguments().push_back(this_expr);

for(const auto &op : as_const(code).operands())

function_call.arguments().push_back(op);

// done building the expression, check the argument types

typecheck_function_call_arguments(function_call);

if(symbol_expr.get_bool(ID_C_not_accessible))

{

const irep_idt &access = symbol_expr.get(ID_C_access);

CHECK_RETURN(

access == ID_private || access == ID_protected ||

access == ID_noaccess);

if(access == ID_private || access == ID_noaccess)

{

#if 0

error().source_location=code.find_source_location();

error() << "constructor of '"

<< to_string(symbol_expr)

<< "' is not accessible" << eom;

throw 0;

#endif

}

}

code_expressiont code_expression(function_call);

code.swap(code_expression);

}

else

{

// a reference member

if(

symbol_expr.id() == ID_dereference &&

to_dereference_expr(symbol_expr).pointer().id() == ID_member &&

symbol_expr.get_bool(ID_C_implicit))

{

// treat references as normal pointers

exprt tmp = to_dereference_expr(symbol_expr).pointer();

symbol_expr.swap(tmp);

}

if(symbol_expr.id() == ID_symbol &&

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

{

// maybe the name of the member collides with a parameter of the

// constructor

exprt dereference(

ID_dereference,

to_pointer_type(cpp_scopes.current_scope().this_expr.type())

.base_type());

dereference.copy_to_operands(cpp_scopes.current_scope().this_expr);

cpp_typecheck_fargst deref_fargs;

deref_fargs.add_object(dereference);

{

cpp_save_scopet cpp_saved_scope(cpp_scopes);

cpp_scopes.go_to(

*(cpp_scopes.id_map[cpp_scopes.current_scope().class_identifier]));

symbol_expr =

resolve(member, cpp_typecheck_resolvet::wantt::VAR, deref_fargs);

}

if(

symbol_expr.id() == ID_dereference &&

to_dereference_expr(symbol_expr).pointer().id() == ID_member &&

symbol_expr.get_bool(ID_C_implicit))

{

// treat references as normal pointers

exprt tmp = to_dereference_expr(symbol_expr).pointer();

symbol_expr.swap(tmp);

}

}

if(

symbol_expr.id() == ID_member &&

to_member_expr(symbol_expr).op().id() == ID_dereference &&

to_dereference_expr(to_member_expr(symbol_expr).op()).pointer() ==

cpp_scopes.current_scope().this_expr)

{

if(is_reference(symbol_expr.type()))

{

// it's a reference member

if(code.operands().size()!= 1)

{

error().source_location=code.find_source_location();

error() << " reference '" << to_string(symbol_expr)

<< "' expects one initializer" << eom;

throw 0;

}

reference_initializer(

code.op0(), to_reference_type(symbol_expr.type()));

// assign the pointers

symbol_expr.type().remove(ID_C_reference);

symbol_expr.set(ID_C_lvalue, true);

code.op0().type().remove(ID_C_reference);

side_effect_exprt assign(

ID_assign,

{symbol_expr, code.op0()},

typet(),

code.source_location());

typecheck_side_effect_assignment(assign);

code_expressiont new_code(assign);

code.swap(new_code);

}

else

{

// it's a data member

already_typechecked_exprt::make_already_typechecked(symbol_expr);

auto call =

cpp_constructor(code.source_location(), symbol_expr, code.operands());

if(call.has_value())

code.swap(call.value());

else

{

auto source_location = code.source_location();

code = code_skipt();

code.add_source_location() = source_location;

}

}

}

else

{

error().source_location=code.find_source_location();

error() << "invalid member initializer '" << to_string(symbol_expr) << "'"

<< eom;

throw 0;

}

}

{

if(code.operands().size()!=1)

{

error().source_location=code.find_source_location();

error() << "declaration expected to have one operand" << eom;

throw 0;

}

PRECONDITION(code.op0().id() == ID_cpp_declaration);

cpp_declarationt &declaration=

to_cpp_declaration(code.op0());

typet &type=declaration.type();

bool is_typedef=declaration.is_typedef();

if(declaration.declarators().empty() || !has_auto(type))

typecheck_type(type);

CHECK_RETURN(type.is_not_nil());

if(

declaration.declarators().empty() &&

((type.id() == ID_struct_tag &&

follow_tag(to_struct_tag_type(type)).get_bool(ID_C_is_anonymous)) ||

(type.id() == ID_union_tag &&

follow_tag(to_union_tag_type(type)).get_bool(ID_C_is_anonymous)) ||

type.get_bool(ID_C_is_anonymous)))

{

if(type.id() != ID_union_tag)

{

error().source_location=code.find_source_location();

error() << "declaration statement does not declare anything"

<< eom;

throw 0;

}

code = convert_anonymous_union(declaration);

return;

}

// mark as 'already typechecked'

already_typechecked_typet::make_already_typechecked(type);

codet new_code(ID_decl_block);

new_code.reserve_operands(declaration.declarators().size());

// Do the declarators (if any)

for(auto &declarator : declaration.declarators())

{

cpp_declarator_convertert cpp_declarator_converter(*this);

cpp_declarator_converter.is_typedef=is_typedef;

const symbolt &symbol=

cpp_declarator_converter.convert(declaration, declarator);

if(is_typedef)

continue;

if(!symbol.is_type && !symbol.is_extern && symbol.type.id() == ID_empty)

{

error().source_location = symbol.location;

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

throw 0;

}

code_frontend_declt decl_statement(cpp_symbol_expr(symbol));

decl_statement.add_source_location()=symbol.location;

// Do we have an initializer that's not code?

if(symbol.value.is_not_nil() &&

symbol.value.id()!=ID_code)

{

decl_statement.copy_to_operands(symbol.value);

DATA_INVARIANT(

has_auto(symbol.type) || decl_statement.op1().type() == symbol.type,

"declarator type should match symbol type");

}

new_code.add_to_operands(std::move(decl_statement));

// is there a constructor to be called?

if(symbol.value.is_not_nil())

{

DATA_INVARIANT(

declarator.find(ID_init_args).is_nil(),

"declarator should not have init_args");

if(symbol.value.id()==ID_code)

new_code.copy_to_operands(symbol.value);

}

else

{

exprt object_expr=cpp_symbol_expr(symbol);

already_typechecked_exprt::make_already_typechecked(object_expr);

auto constructor_call = cpp_constructor(

symbol.location, object_expr, declarator.init_args().operands());

if(constructor_call.has_value())

new_code.add_to_operands(std::move(constructor_call.value()));

}

}

code.swap(new_code);

{

cpp_save_scopet saved_scope(cpp_scopes);

cpp_scopes.new_block_scope();

c_typecheck_baset::typecheck_block(code);