diff --git a/jbmc/src/java_bytecode/java_bytecode_instrument.cpp b/jbmc/src/java_bytecode/java_bytecode_instrument.cpp index f0aae000897..76ee70ee262 100644 --- a/jbmc/src/java_bytecode/java_bytecode_instrument.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_instrument.cpp @@ -604,13 +604,14 @@ void java_bytecode_instrument_uncaught_exceptions( const source_locationt &source_location) { // check that there is no uncaught exception - code_assertt assert_no_exception; - assert_no_exception.assertion() = equal_exprt( + code_assertt assert_no_exception(equal_exprt( exc_symbol.symbol_expr(), - null_pointer_exprt(to_pointer_type(exc_symbol.type))); + null_pointer_exprt(to_pointer_type(exc_symbol.type)))); + source_locationt assert_location = source_location; assert_location.set_comment("no uncaught exception"); assert_no_exception.add_source_location() = assert_location; + init_code.move_to_operands(assert_no_exception); } diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp index a591883ad24..e3d3aa9620d 100644 --- a/src/ansi-c/c_typecheck_code.cpp +++ b/src/ansi-c/c_typecheck_code.cpp @@ -322,9 +322,8 @@ void c_typecheck_baset::typecheck_decl(codet &code) } else { - code_declt code; + code_declt code(symbol.symbol_expr()); code.add_source_location()=symbol.location; - code.symbol()=symbol.symbol_expr(); code.symbol().add_source_location()=symbol.location; // add initializer, if any diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 4c8b9e838fb..41ca6295f12 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -461,14 +461,14 @@ void c_typecheck_baset::typecheck_expr_builtin_va_arg(exprt &expr) implicit_typecast(arg, pointer_type(void_type())); + symbol_exprt function(ID_gcc_builtin_va_arg, new_type); + function.add_source_location() = expr.source_location(); + // turn into function call - side_effect_expr_function_callt result; + side_effect_expr_function_callt result( + function, {arg}, new_type.return_type()); + result.add_source_location()=expr.source_location(); - result.function()=symbol_exprt(ID_gcc_builtin_va_arg); - result.function().add_source_location()=expr.source_location(); - result.function().type()=new_type; - result.arguments().push_back(arg); - result.type()=new_type.return_type(); expr.swap(result); @@ -724,9 +724,8 @@ void c_typecheck_baset::typecheck_expr_operands(exprt &expr) throw 0; } - code_declt decl; + code_declt decl(symbol.symbol_expr()); decl.add_source_location()=declaration.source_location(); - decl.symbol()=symbol.symbol_expr(); expr.op0()=decl; @@ -882,15 +881,13 @@ void c_typecheck_baset::typecheck_side_effect_statement_expression( code_function_callt &fc=to_code_function_call(last); - side_effect_expr_function_callt sideeffect; + auto return_type = + static_cast(fc.function().type().find(ID_return_type)); - sideeffect.function()=fc.function(); - sideeffect.arguments()=fc.arguments(); + side_effect_expr_function_callt sideeffect( + fc.function(), fc.arguments(), return_type); sideeffect.add_source_location()=fc.source_location(); - sideeffect.type()= - static_cast(fc.function().type().find(ID_return_type)); - expr.type()=sideeffect.type(); if(fc.lhs().is_nil()) diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index 4960c54602f..dc94036ec6d 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -324,8 +324,7 @@ void goto_convertt::do_input( const exprt::operandst &arguments, goto_programt &dest) { - codet input_code; - input_code.set_statement(ID_input); + codet input_code(ID_input); input_code.operands()=arguments; input_code.add_source_location()=function.source_location(); @@ -344,8 +343,7 @@ void goto_convertt::do_output( const exprt::operandst &arguments, goto_programt &dest) { - codet output_code; - output_code.set_statement(ID_output); + codet output_code(ID_output); output_code.operands()=arguments; output_code.add_source_location()=function.source_location(); @@ -605,8 +603,7 @@ void goto_convertt::do_array_op( throw 0; } - codet array_op_statement; - array_op_statement.set_statement(id); + codet array_op_statement(id); array_op_statement.operands()=arguments; array_op_statement.add_source_location()=function.source_location(); diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 0dbe67d20b5..81790b3169f 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -1990,8 +1990,7 @@ symbolt &goto_convertt::new_tmp_symbol( mode, symbol_table); - code_declt decl; - decl.symbol()=new_symbol.symbol_expr(); + code_declt decl(new_symbol.symbol_expr()); decl.add_source_location()=source_location; convert_decl(decl, dest, mode); diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp index 1869e906cb7..2aeab13da62 100644 --- a/src/goto-programs/goto_convert_side_effect.cpp +++ b/src/goto-programs/goto_convert_side_effect.cpp @@ -390,8 +390,7 @@ void goto_convertt::remove_function_call( symbol_table); { - code_declt decl; - decl.symbol()=new_symbol.symbol_expr(); + code_declt decl(new_symbol.symbol_expr()); decl.add_source_location()=new_symbol.location; convert_decl(decl, dest, mode); } @@ -425,8 +424,6 @@ void goto_convertt::remove_cpp_new( goto_programt &dest, bool result_is_used) { - codet call; - const symbolt &new_symbol = get_fresh_aux_symbol( expr.type(), tmp_symbol_prefix, @@ -435,12 +432,11 @@ void goto_convertt::remove_cpp_new( ID_cpp, symbol_table); - code_declt decl; - decl.symbol()=new_symbol.symbol_expr(); + code_declt decl(new_symbol.symbol_expr()); decl.add_source_location()=new_symbol.location; convert_decl(decl, dest, ID_cpp); - call=code_assignt(new_symbol.symbol_expr(), expr); + const code_assignt call(new_symbol.symbol_expr(), expr); if(result_is_used) static_cast(expr)=new_symbol.symbol_expr(); @@ -456,9 +452,7 @@ void goto_convertt::remove_cpp_delete( { assert(expr.operands().size()==1); - codet tmp; - - tmp.set_statement(expr.get_statement()); + codet tmp(expr.get_statement()); tmp.add_source_location()=expr.source_location(); tmp.copy_to_operands(expr.op0()); tmp.set(ID_destructor, expr.find(ID_destructor)); diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp index 7f1ef61dce2..8a289e5bbe0 100644 --- a/src/goto-programs/remove_function_pointers.cpp +++ b/src/goto-programs/remove_function_pointers.cpp @@ -420,9 +420,8 @@ void remove_function_pointerst::remove_function_pointer( // We preserve the original dereferencing to possibly catch // further pointer-related errors. - code_expressiont code_expression; + code_expressiont code_expression(function); code_expression.add_source_location()=function.source_location(); - code_expression.expression()=function; target->code.swap(code_expression); target->type=OTHER; diff --git a/src/util/std_code.cpp b/src/util/std_code.cpp index a280f83d064..1bdd6763ba0 100644 --- a/src/util/std_code.cpp +++ b/src/util/std_code.cpp @@ -29,8 +29,7 @@ code_blockt &codet::make_block() exprt tmp; tmp.swap(*this); - *this=codet(); - set_statement(ID_block); + *this = codet(ID_block); move_to_operands(tmp); return static_cast(*this); diff --git a/src/util/std_code.h b/src/util/std_code.h index 422a492896e..99640a12423 100644 --- a/src/util/std_code.h +++ b/src/util/std_code.h @@ -21,6 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com class codet:public exprt { public: + DEPRECATED("Use codet(statement) instead") codet():exprt(ID_code, typet(ID_code)) { } @@ -253,6 +254,7 @@ inline code_assignt &to_code_assign(codet &code) class code_declt:public codet { public: + DEPRECATED("Use code_declt(symbol) instead") code_declt():codet(ID_decl) { operands().resize(1); @@ -305,6 +307,7 @@ inline code_declt &to_code_decl(codet &code) class code_deadt:public codet { public: + DEPRECATED("Use code_deadt(symbol) instead") code_deadt():codet(ID_dead) { operands().resize(1); @@ -354,6 +357,7 @@ inline code_deadt &to_code_dead(codet &code) class code_assumet:public codet { public: + DEPRECATED("Use code_assumet(expr) instead") code_assumet():codet(ID_assume) { operands().resize(1); @@ -400,6 +404,7 @@ inline code_assumet &to_code_assume(codet &code) class code_assertt:public codet { public: + DEPRECATED("Use code_assertt(expr) instead") code_assertt():codet(ID_assert) { operands().resize(1); @@ -533,11 +538,19 @@ inline code_ifthenelset &to_code_ifthenelse(codet &code) class code_switcht:public codet { public: + DEPRECATED("Use code_switcht(value, body) instead") code_switcht():codet(ID_switch) { operands().resize(2); } + code_switcht(const exprt &_value, const codet &_body) : codet(ID_switch) + { + operands().resize(2); + value() = _value; + body() = _body; + } + const exprt &value() const { return op0(); @@ -588,11 +601,19 @@ inline code_switcht &to_code_switch(codet &code) class code_whilet:public codet { public: + DEPRECATED("Use code_whilet(cond, body) instead") code_whilet():codet(ID_while) { operands().resize(2); } + code_whilet(const exprt &_cond, const codet &_body) : codet(ID_while) + { + operands().resize(2); + cond() = _cond; + body() = _body; + } + const exprt &cond() const { return op0(); @@ -643,11 +664,19 @@ inline code_whilet &to_code_while(codet &code) class code_dowhilet:public codet { public: + DEPRECATED("Use code_dowhilet(cond, body) instead") code_dowhilet():codet(ID_dowhile) { operands().resize(2); } + code_dowhilet(const exprt &_cond, const codet &_body) : codet(ID_dowhile) + { + operands().resize(2); + cond() = _cond; + body() = _body; + } + const exprt &cond() const { return op0(); @@ -774,6 +803,7 @@ inline code_fort &to_code_for(codet &code) class code_gotot:public codet { public: + DEPRECATED("Use code_gotot(label) instead") code_gotot():codet(ID_goto) { } @@ -947,6 +977,7 @@ inline code_returnt &to_code_return(codet &code) class code_labelt:public codet { public: + DEPRECATED("Use code_labelt(label) instead") code_labelt():codet(ID_label) { operands().resize(1); @@ -1014,6 +1045,7 @@ inline code_labelt &to_code_label(codet &code) class code_switch_caset:public codet { public: + DEPRECATED("Use code_switch_caset(case_op, code) instead") code_switch_caset():codet(ID_switch_case) { operands().resize(2); @@ -1188,6 +1220,7 @@ inline const code_asmt &to_code_asm(const codet &code) class code_expressiont:public codet { public: + DEPRECATED("Use code_expressiont(expr) instead") code_expressiont():codet(ID_expression) { operands().resize(1); @@ -1238,6 +1271,7 @@ inline const code_expressiont &to_code_expression(const codet &code) class side_effect_exprt:public exprt { public: + DEPRECATED("Use side_effect_exprt(statement, type) instead") explicit side_effect_exprt(const irep_idt &statement): exprt(ID_side_effect) { @@ -1301,6 +1335,7 @@ inline const side_effect_exprt &to_side_effect_expr(const exprt &expr) class side_effect_expr_nondett:public side_effect_exprt { public: + DEPRECATED("Use side_effect_expr_nondett(statement, type) instead") side_effect_expr_nondett():side_effect_exprt(ID_nondet) { set_nullable(true); @@ -1352,12 +1387,36 @@ inline const side_effect_expr_nondett &to_side_effect_expr_nondet( class side_effect_expr_function_callt:public side_effect_exprt { public: + DEPRECATED("Use side_effect_expr_function_callt(...) instead") side_effect_expr_function_callt():side_effect_exprt(ID_function_call) { operands().resize(2); op1().id(ID_arguments); } + side_effect_expr_function_callt( + const exprt &_function, + const exprt::operandst &_arguments) + : side_effect_exprt(ID_function_call) + { + operands().resize(2); + op1().id(ID_arguments); + function() = _function; + arguments() = _arguments; + } + + side_effect_expr_function_callt( + const exprt &_function, + const exprt::operandst &_arguments, + const typet &_type) + : side_effect_exprt(ID_function_call, _type) + { + operands().resize(2); + op1().id(ID_arguments); + function() = _function; + arguments() = _arguments; + } + exprt &function() { return op0(); @@ -1409,6 +1468,7 @@ inline const side_effect_expr_function_callt class side_effect_expr_throwt:public side_effect_exprt { public: + DEPRECATED("Use side_effect_expr_throwt(exception_list) instead") side_effect_expr_throwt():side_effect_exprt(ID_throw) { }