diff --git a/src/cpp/cpp_constructor.cpp b/src/cpp/cpp_constructor.cpp index ea1670035a9..78eb37606c0 100644 --- a/src/cpp/cpp_constructor.cpp +++ b/src/cpp/cpp_constructor.cpp @@ -22,7 +22,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu /// \param object: non-typechecked object /// \param operands: non-typechecked operands /// \return typechecked code -codet cpp_typecheckt::cpp_constructor( +optionalt cpp_typecheckt::cpp_constructor( const source_locationt &source_location, const exprt &object, const exprt::operandst &operands) @@ -56,22 +56,13 @@ codet cpp_typecheckt::cpp_constructor( assert(operands.empty() || operands.size()==1); if(operands.empty() && cpp_is_pod(tmp_type)) - { - codet nil; - nil.make_nil(); - return nil; - } + return {}; const exprt &size_expr= to_array_type(tmp_type).size(); if(size_expr.id() == ID_infinity) - { - // don't initialize - codet nil; - nil.make_nil(); - return nil; - } + return {}; // don't initialize exprt tmp_size=size_expr; make_constant_index(tmp_size); @@ -122,23 +113,16 @@ codet cpp_typecheckt::cpp_constructor( tmp_operands.push_back(operand); } - exprt i_code = - cpp_constructor(source_location, index, tmp_operands); - - if(i_code.is_nil()) - { - new_code.is_nil(); - break; - } + auto i_code = cpp_constructor(source_location, index, tmp_operands); - new_code.move_to_operands(i_code); + if(i_code.has_value()) + new_code.move(i_code.value()); } return new_code; } } else if(cpp_is_pod(tmp_type)) { - code_expressiont new_code; exprt::operandst operands_tc=operands; for(exprt::operandst::iterator @@ -153,7 +137,7 @@ codet cpp_typecheckt::cpp_constructor( if(operands_tc.empty()) { // a POD is NOT initialized - new_code.make_nil(); + return {}; } else if(operands_tc.size()==1) { @@ -163,7 +147,9 @@ codet cpp_typecheckt::cpp_constructor( side_effect_exprt assign(ID_assign, typet(), source_location); assign.copy_to_operands(object_tc, operands_tc.front()); typecheck_side_effect_assignment(assign); + code_expressiont new_code; new_code.expression()=assign; + return new_code; } else { @@ -172,8 +158,6 @@ codet cpp_typecheckt::cpp_constructor( "but got " << operands.size() << eom; throw 0; } - - return new_code; } else if(tmp_type.id()==ID_union) { @@ -293,9 +277,7 @@ codet cpp_typecheckt::cpp_constructor( else UNREACHABLE; - codet nil; - nil.make_nil(); - return nil; + return {}; } void cpp_typecheckt::new_temporary( @@ -316,15 +298,14 @@ void cpp_typecheckt::new_temporary( already_typechecked(new_object); - codet new_code = - cpp_constructor(source_location, new_object, ops); + auto new_code = cpp_constructor(source_location, new_object, ops); - if(new_code.is_not_nil()) + if(new_code.has_value()) { - if(new_code.get(ID_statement)==ID_assign) - tmp_object_expr.move_to_operands(new_code.op1()); + if(new_code->get_statement() == ID_assign) + tmp_object_expr.move_to_operands(new_code->op1()); else - tmp_object_expr.add(ID_initializer)=new_code; + tmp_object_expr.add(ID_initializer) = *new_code; } temporary.swap(tmp_object_expr); diff --git a/src/cpp/cpp_destructor.cpp b/src/cpp/cpp_destructor.cpp index 49704869ee8..4a64333f3a0 100644 --- a/src/cpp/cpp_destructor.cpp +++ b/src/cpp/cpp_destructor.cpp @@ -16,7 +16,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include /// \return typechecked code -codet cpp_typecheckt::cpp_destructor( +optionalt cpp_typecheckt::cpp_destructor( const source_locationt &source_location, const exprt &object) { @@ -31,10 +31,7 @@ codet cpp_typecheckt::cpp_destructor( // PODs don't need a destructor if(cpp_is_pod(tmp_type)) - { - new_code.make_nil(); - return new_code; - } + return {}; if(tmp_type.id()==ID_array) { @@ -42,11 +39,7 @@ codet cpp_typecheckt::cpp_destructor( to_array_type(tmp_type).size(); if(size_expr.id()=="infinity") - { - // don't initialize - new_code.make_nil(); - return new_code; - } + return {}; // don't initialize exprt tmp_size=size_expr; make_constant_index(tmp_size); @@ -73,9 +66,9 @@ codet cpp_typecheckt::cpp_destructor( index_exprt index(object, constant); index.add_source_location()=source_location; - exprt i_code = cpp_destructor(source_location, index); - - new_code.move_to_operands(i_code); + auto i_code = cpp_destructor(source_location, index); + if(i_code.has_value()) + new_code.move_to_operands(i_code.value()); } } else diff --git a/src/cpp/cpp_typecheck.cpp b/src/cpp/cpp_typecheck.cpp index 055090eb5e7..02c9c451d56 100644 --- a/src/cpp/cpp_typecheck.cpp +++ b/src/cpp/cpp_typecheck.cpp @@ -188,11 +188,10 @@ void cpp_typecheckt::static_and_dynamic_initialization() // use default constructor exprt::operandst ops; - codet call= - cpp_constructor(symbol.location, symbol_expr, ops); + auto call = cpp_constructor(symbol.location, symbol_expr, ops); - if(call.is_not_nil()) - init_block.move_to_operands(call); + if(call.has_value()) + init_block.move(call.value()); } } diff --git a/src/cpp/cpp_typecheck.h b/src/cpp/cpp_typecheck.h index 08e078017e8..e3935d82605 100644 --- a/src/cpp/cpp_typecheck.h +++ b/src/cpp/cpp_typecheck.h @@ -99,7 +99,7 @@ class cpp_typecheckt:public c_typecheck_baset bool cpp_is_pod(const typet &type) const; - codet cpp_constructor( + optionalt cpp_constructor( const source_locationt &source_location, const exprt &object, const exprt::operandst &operands); @@ -427,9 +427,8 @@ class cpp_typecheckt:public c_typecheck_baset const struct_typet &this_struct_type(); - codet cpp_destructor( - const source_locationt &source_location, - const exprt &object); + optionalt + cpp_destructor(const source_locationt &source_location, const exprt &object); // expressions void explicit_typecast_ambiguity(exprt &expr); diff --git a/src/cpp/cpp_typecheck_code.cpp b/src/cpp/cpp_typecheck_code.cpp index 924c189b80f..8686cf8813b 100644 --- a/src/cpp/cpp_typecheck_code.cpp +++ b/src/cpp/cpp_typecheck_code.cpp @@ -327,16 +327,17 @@ void cpp_typecheckt::typecheck_member_initializer(codet &code) // it's a data member already_typechecked(symbol_expr); - exprt call= + auto call = cpp_constructor(code.source_location(), symbol_expr, code.operands()); - if(call.is_nil()) + if(call.has_value()) + code.swap(call.value()); + else { - call=codet(ID_skip); - call.add_source_location()=code.source_location(); + auto source_location = code.source_location(); + code = codet(ID_skip); + code.add_source_location() = source_location; } - - code.swap(call); } } else @@ -434,14 +435,11 @@ void cpp_typecheckt::typecheck_decl(codet &code) already_typechecked(object_expr); - exprt constructor_call= - cpp_constructor( - symbol.location, - object_expr, - declarator.init_args().operands()); + auto constructor_call = cpp_constructor( + symbol.location, object_expr, declarator.init_args().operands()); - if(constructor_call.is_not_nil()) - new_code.move_to_operands(constructor_call); + if(constructor_call.has_value()) + new_code.move_to_operands(constructor_call.value()); } } diff --git a/src/cpp/cpp_typecheck_compound_type.cpp b/src/cpp/cpp_typecheck_compound_type.cpp index 0422bcfffab..991220e54a8 100644 --- a/src/cpp/cpp_typecheck_compound_type.cpp +++ b/src/cpp/cpp_typecheck_compound_type.cpp @@ -740,10 +740,10 @@ void cpp_typecheckt::typecheck_compound_declarator( exprt::operandst ops; ops.push_back(value); - codet defcode = - cpp_constructor(source_locationt(), symexpr, ops); + auto defcode = cpp_constructor(source_locationt(), symexpr, ops); + CHECK_RETURN(defcode.has_value()); - new_symbol->value.swap(defcode); + new_symbol->value.swap(defcode.value()); } } } diff --git a/src/cpp/cpp_typecheck_declaration.cpp b/src/cpp/cpp_typecheck_declaration.cpp index 9c6fc9b9e9f..c8cabc9ab11 100644 --- a/src/cpp/cpp_typecheck_declaration.cpp +++ b/src/cpp/cpp_typecheck_declaration.cpp @@ -178,11 +178,15 @@ void cpp_typecheckt::convert_non_template_declaration( if(symbol.is_lvalue && declarator.init_args().has_operands()) { - symbol.value= - cpp_constructor( - symbol.location, - cpp_symbol_expr(symbol), - declarator.init_args().operands()); + auto constructor = cpp_constructor( + symbol.location, + cpp_symbol_expr(symbol), + declarator.init_args().operands()); + + if(constructor.has_value()) + symbol.value = constructor.value(); + else + symbol.value = nil_exprt(); } } } diff --git a/src/cpp/cpp_typecheck_destructor.cpp b/src/cpp/cpp_typecheck_destructor.cpp index 8f66277be04..0b06b6f95d7 100644 --- a/src/cpp/cpp_typecheck_destructor.cpp +++ b/src/cpp/cpp_typecheck_destructor.cpp @@ -144,11 +144,11 @@ codet cpp_typecheckt::dtor(const symbolt &symbol) const bool disabled_access_control = disable_access_control; disable_access_control = true; - codet dtor_code = cpp_destructor(source_location, member); + auto dtor_code = cpp_destructor(source_location, member); disable_access_control = disabled_access_control; - if(dtor_code.is_not_nil()) - block.move_to_operands(dtor_code); + if(dtor_code.has_value()) + block.move_to_operands(dtor_code.value()); } const irept::subt &bases=symbol.type.find(ID_bases).get_sub(); @@ -169,11 +169,11 @@ codet cpp_typecheckt::dtor(const symbolt &symbol) const bool disabled_access_control = disable_access_control; disable_access_control = true; - exprt dtor_code = cpp_destructor(source_location, object); + auto dtor_code = cpp_destructor(source_location, object); disable_access_control = disabled_access_control; - if(dtor_code.is_not_nil()) - block.move_to_operands(dtor_code); + if(dtor_code.has_value()) + block.move_to_operands(dtor_code.value()); } return block; diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp index b8204c597f6..b6a9803e905 100644 --- a/src/cpp/cpp_typecheck_expr.cpp +++ b/src/cpp/cpp_typecheck_expr.cpp @@ -852,13 +852,13 @@ void cpp_typecheckt::typecheck_expr_new(exprt &expr) throw 0; } - exprt code= - cpp_constructor( - expr.find_source_location(), - object_expr, - initializer.operands()); + auto code = cpp_constructor( + expr.find_source_location(), object_expr, initializer.operands()); - expr.add(ID_initializer).swap(code); + if(code.has_value()) + expr.add(ID_initializer).swap(code.value()); + else + expr.add(ID_initializer) = nil_exprt(); // we add the size of the object for convenience of the // runtime library @@ -1074,15 +1074,16 @@ void cpp_typecheckt::typecheck_expr_delete(exprt &expr) already_typechecked(new_object); - codet destructor_code=cpp_destructor( - expr.source_location(), - new_object); - - // this isn't typechecked yet - if(destructor_code.is_not_nil()) - typecheck_code(destructor_code); + auto destructor_code = cpp_destructor(expr.source_location(), new_object); - expr.set(ID_destructor, destructor_code); + if(destructor_code.has_value()) + { + // this isn't typechecked yet + typecheck_code(destructor_code.value()); + expr.set(ID_destructor, destructor_code.value()); + } + else + expr.set(ID_destructor, nil_exprt()); } void cpp_typecheckt::typecheck_expr_typecast(exprt &) diff --git a/src/cpp/cpp_typecheck_initializer.cpp b/src/cpp/cpp_typecheck_initializer.cpp index 69f91885c36..3ca9dd957e3 100644 --- a/src/cpp/cpp_typecheck_initializer.cpp +++ b/src/cpp/cpp_typecheck_initializer.cpp @@ -180,10 +180,13 @@ void cpp_typecheckt::convert_initializer(symbolt &symbol) exprt::operandst ops; ops.push_back(symbol.value); - symbol.value = cpp_constructor( - symbol.value.source_location(), - expr_symbol, - ops); + auto constructor = + cpp_constructor(symbol.value.source_location(), expr_symbol, ops); + + if(constructor.has_value()) + symbol.value = constructor.value(); + else + symbol.value = nil_exprt(); } }