diff --git a/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp b/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp index 380282d32ff..3c9cb677d7f 100644 --- a/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp @@ -122,11 +122,7 @@ static codet get_monitor_call( return code_skipt(); // Otherwise we create a function call - code_function_callt call; - call.function() = symbol_exprt(symbol, it->second.type); - call.lhs().make_nil(); - call.arguments().push_back(object); - return call; + return code_function_callt(symbol_exprt(symbol, it->second.type), {object}); } /// Introduces a monitorexit before every return recursively. @@ -288,11 +284,15 @@ static void instrument_start_thread( // Create global variable __CPROVER__next_thread_id. Used as a counter // in-order to to assign ids to new threads. - const symbolt &next_symbol = - add_or_get_symbol( - symbol_table, next_thread_id, next_thread_id, - java_int_type(), - from_integer(0, java_int_type()), false, true); + const symbol_exprt next_symbol_expr = add_or_get_symbol( + symbol_table, + next_thread_id, + next_thread_id, + java_int_type(), + from_integer(0, java_int_type()), + false, + true) + .symbol_expr(); // Create thread-local variable __CPROVER__thread_id. Holds the id of // the thread. @@ -320,14 +320,11 @@ static void instrument_start_thread( codet tmp_a(ID_start_thread); tmp_a.set(ID_destination, lbl1); code_gotot tmp_b(lbl2); - code_labelt tmp_c(lbl1); - tmp_c.op0() = codet(ID_skip); + const code_labelt tmp_c(lbl1, code_skipt()); - exprt plus(ID_plus, java_int_type()); - plus.copy_to_operands(next_symbol.symbol_expr()); - plus.copy_to_operands(from_integer(1, java_int_type())); - code_assignt tmp_d(next_symbol.symbol_expr(), plus); - code_assignt tmp_e(current_symbol.symbol_expr(), next_symbol.symbol_expr()); + const plus_exprt plus(next_symbol_expr, from_integer(1, java_int_type())); + const code_assignt tmp_d(next_symbol_expr, plus); + const code_assignt tmp_e(current_symbol.symbol_expr(), next_symbol_expr); code_blockt block; block.add(tmp_a); @@ -368,8 +365,7 @@ static void instrument_end_thread( // A: codet(id=ID_end_thread) // B: codet(id=ID_label,label= __CPROVER_THREAD_EXIT_) codet tmp_a(ID_end_thread); - code_labelt tmp_b(lbl2); - tmp_b.op0() = codet(ID_skip); + const code_labelt tmp_b(lbl2, code_skipt()); code_blockt block; block.add(tmp_a); diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 73471142593..c2b4241ebdd 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -973,8 +973,7 @@ codet java_bytecode_convert_methodt::get_clinit_call( return code_skipt(); else { - code_function_callt ret; - ret.function() = findit->second.symbol_expr(); + const code_function_callt ret(findit->second.symbol_expr()); if(needed_lazy_methods) needed_lazy_methods->add_needed_method(findit->second.name); return ret; @@ -2004,10 +2003,7 @@ codet java_bytecode_convert_methodt::convert_monitorenterexit( java_method_typet type( {java_method_typet::parametert(java_reference_type(void_typet()))}, void_typet()); - code_function_callt call; - call.function() = symbol_exprt(descriptor, type); - call.lhs().make_nil(); - call.arguments().push_back(op[0]); + code_function_callt call(symbol_exprt(descriptor, type), {op[0]}); call.add_source_location() = source_location; if(needed_lazy_methods && symbol_table.has_symbol(descriptor)) needed_lazy_methods->add_needed_method(descriptor); @@ -2737,13 +2733,11 @@ codet java_bytecode_convert_methodt::convert_iinc( bytecode_write_typet::VARIABLE, to_symbol_expr(locvar).get_identifier()); - code_assignt code_assign; - code_assign.lhs() = variable(arg0, 'i', address, NO_CAST); - exprt arg1_int_type = arg1; - if(arg1.type() != java_int_type()) - arg1_int_type.make_typecast(java_int_type()); - code_assign.rhs() = - plus_exprt(variable(arg0, 'i', address, CAST_AS_NEEDED), arg1_int_type); + const exprt arg1_int_type = + typecast_exprt::conditional_cast(arg1, java_int_type()); + const code_assignt code_assign( + variable(arg0, 'i', address, NO_CAST), + plus_exprt(variable(arg0, 'i', address, CAST_AS_NEEDED), arg1_int_type)); block.copy_to_operands(code_assign); return block; } diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp index 192b0a92e19..75ceefa9c7b 100644 --- a/jbmc/src/java_bytecode/java_entry_point.cpp +++ b/jbmc/src/java_bytecode/java_entry_point.cpp @@ -169,33 +169,26 @@ static void java_static_lifetime_init( // Argument order is: name, isAnnotation, isArray, isInterface, // isSynthetic, isLocalClass, isMemberClass, isEnum - code_function_callt initializer_call; - initializer_call.function() = class_literal_init_method->symbol_expr(); - - code_function_callt::argumentst &args = initializer_call.arguments(); - - // this: - args.push_back(address_of_exprt(sym.symbol_expr())); - // name: - args.push_back(address_of_exprt(class_name_literal)); - // isAnnotation: - args.push_back( - constant_bool(class_symbol.type.get_bool(ID_is_annotation))); - // isArray: - args.push_back(constant_bool(class_is_array)); - // isInterface: - args.push_back( - constant_bool(class_symbol.type.get_bool(ID_interface))); - // isSynthetic: - args.push_back( - constant_bool(class_symbol.type.get_bool(ID_synthetic))); - // isLocalClass: - args.push_back(nondet_bool); - // isMemberClass: - args.push_back(nondet_bool); - // isEnum: - args.push_back( - constant_bool(class_symbol.type.get_bool(ID_enumeration))); + code_function_callt initializer_call( + class_literal_init_method->symbol_expr(), + {// this: + address_of_exprt(sym.symbol_expr()), + // name: + address_of_exprt(class_name_literal), + // isAnnotation: + constant_bool(class_symbol.type.get_bool(ID_is_annotation)), + // isArray: + constant_bool(class_is_array), + // isInterface: + constant_bool(class_symbol.type.get_bool(ID_interface)), + // isSynthetic: + constant_bool(class_symbol.type.get_bool(ID_synthetic)), + // isLocalClass: + nondet_bool, + // isMemberClass: + nondet_bool, + // isEnum: + constant_bool(class_symbol.type.get_bool(ID_enumeration))}); // First initialize the object as prior to a constructor: namespacet ns(symbol_table); @@ -676,10 +669,8 @@ bool generate_java_start_function( return true; // give up with error } - code_function_callt call_init; - call_init.lhs().make_nil(); + code_function_callt call_init(init_it->second.symbol_expr()); call_init.add_source_location()=symbol.location; - call_init.function()=init_it->second.symbol_expr(); init_code.move_to_operands(call_init); } @@ -689,15 +680,13 @@ bool generate_java_start_function( // where return is a new variable // and arg1 ... argn are constructed below as well - code_function_callt call_main; - source_locationt loc=symbol.location; loc.set_function(symbol.name); source_locationt &dloc=loc; // function to call + code_function_callt call_main(symbol.symbol_expr()); call_main.add_source_location()=dloc; - call_main.function()=symbol.symbol_expr(); call_main.function().add_source_location()=dloc; // if the method return type is not void, store return value in a new variable diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index 5d405a0cc3b..f0062589c6e 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -213,7 +213,7 @@ exprt allocate_dynamic_object( ID_java, symbol_table); symbols_created.push_back(&malloc_sym); - code_assignt assign=code_assignt(malloc_sym.symbol_expr(), malloc_expr); + code_assignt assign(malloc_sym.symbol_expr(), malloc_expr); assign.add_source_location()=loc; output_code.copy_to_operands(assign); exprt malloc_symbol_expr=malloc_sym.symbol_expr(); @@ -1392,7 +1392,7 @@ void java_object_factoryt::gen_nondet_array_init( symbol_table); symbols_created.push_back(&array_init_symbol); const auto &array_init_symexpr=array_init_symbol.symbol_expr(); - codet data_assign=code_assignt(array_init_symexpr, init_array_expr); + code_assignt data_assign(array_init_symexpr, init_array_expr); data_assign.add_source_location()=loc; assignments.copy_to_operands(data_assign); @@ -1739,8 +1739,7 @@ void java_object_factoryt::gen_method_call_if_present( if(const auto func = symbol_table.lookup(method_name)) { const java_method_typet &type = to_java_method_type(func->type); - code_function_callt fun_call; - fun_call.function() = func->symbol_expr(); + code_function_callt fun_call(func->symbol_expr()); if(type.has_this()) fun_call.arguments().push_back(address_of_exprt(instance_expr)); assignments.add(fun_call); diff --git a/jbmc/src/java_bytecode/java_static_initializers.cpp b/jbmc/src/java_bytecode/java_static_initializers.cpp index e0f3444a267..0f1d69bd8dd 100644 --- a/jbmc/src/java_bytecode/java_static_initializers.cpp +++ b/jbmc/src/java_bytecode/java_static_initializers.cpp @@ -208,18 +208,16 @@ static void clinit_wrapper_do_recursive_calls( auto findit = symbol_table.symbols.find(base_init_routine); if(findit == symbol_table.symbols.end()) continue; - code_function_callt call_base; - call_base.function() = findit->second.symbol_expr(); - init_body.move_to_operands(call_base); + const code_function_callt call_base(findit->second.symbol_expr()); + init_body.add(call_base); } const irep_idt &real_clinit_name = clinit_function_name(class_name); auto find_sym_it = symbol_table.symbols.find(real_clinit_name); if(find_sym_it != symbol_table.symbols.end()) { - code_function_callt call_real_init; - call_real_init.function() = find_sym_it->second.symbol_expr(); - init_body.move_to_operands(call_real_init); + const code_function_callt call_real_init(find_sym_it->second.symbol_expr()); + init_body.add(call_real_init); } // If nondet-static option is given, add a standard nondet initialization for diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp index ebf92963563..ff2dd7c23e3 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp @@ -1552,11 +1552,11 @@ codet java_string_library_preprocesst::make_object_get_class_code( loc); // > class1 = Class.forName(string1) - code_function_callt fun_call; - fun_call.function()=symbol_exprt( - "java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class;"); - fun_call.lhs()=class1; - fun_call.arguments().push_back(string1); + code_function_callt fun_call( + class1, + symbol_exprt( + "java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class;"), + {string1}); const java_method_typet fun_type( {java_method_typet::parametert(string_ptr_type)}, class_type); fun_call.function().type()=fun_type; diff --git a/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp b/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp index fb294c1d148..c5861c8d9cd 100644 --- a/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp +++ b/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp @@ -129,13 +129,12 @@ SCENARIO( callee.set(ID_C_class, "java::VirtualFunctionsTestParent"); callee.set(ID_component_name, "f:()V"); - code_function_callt call; - call.function() = callee; - // Specific argument doesn't matter, so just pass an appropriately typed - // null pointer: - call.arguments().push_back( - null_pointer_exprt( - to_pointer_type(to_code_type(callee.type()).parameters()[0].type()))); + const code_function_callt call( + callee, + // Specific argument doesn't matter, so just pass an appropriately typed + // null pointer: + {null_pointer_exprt( + to_pointer_type(to_code_type(callee.type()).parameters()[0].type()))}); virtual_call_inst->code = call; test_program.add_instruction(END_FUNCTION); diff --git a/jbmc/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp b/jbmc/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp index 003f866f5f4..d2980d3185f 100644 --- a/jbmc/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp +++ b/jbmc/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp @@ -32,7 +32,7 @@ void check_function_call( for(const auto &target : targets) { REQUIRE(target->type == goto_program_instruction_typet::FUNCTION_CALL); - const code_function_callt call = to_code_function_call(target->code); + const code_function_callt &call = to_code_function_call(target->code); REQUIRE(call.function().id() == ID_symbol); REQUIRE(to_symbol_expr(call.function()).get_identifier() == function_name); } diff --git a/src/cpp/cpp_typecheck_code.cpp b/src/cpp/cpp_typecheck_code.cpp index be71f110fa0..2176710d089 100644 --- a/src/cpp/cpp_typecheck_code.cpp +++ b/src/cpp/cpp_typecheck_code.cpp @@ -334,7 +334,7 @@ void cpp_typecheckt::typecheck_member_initializer(codet &code) else { auto source_location = code.source_location(); - code = codet(ID_skip); + code = code_skipt(); code.add_source_location() = source_location; } } diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp index df89ee357e8..def62d0b308 100644 --- a/src/cpp/parse.cpp +++ b/src/cpp/parse.cpp @@ -8103,7 +8103,7 @@ bool Parser::rExprStatement(codet &statement) #endif lex.get_token(tk); - statement=codet(ID_skip); + statement = code_skipt(); set_location(statement, tk); return true; } diff --git a/src/goto-analyzer/taint_analysis.cpp b/src/goto-analyzer/taint_analysis.cpp index 67539387227..69a35ce08cf 100644 --- a/src/goto-analyzer/taint_analysis.cpp +++ b/src/goto-analyzer/taint_analysis.cpp @@ -281,8 +281,7 @@ bool taint_analysist::operator()( f_it->first!=goto_functionst::entry_point()) { goto_programt::targett t=calls.add_instruction(); - code_function_callt call; - call.function()=ns.lookup(f_it->first).symbol_expr(); + const code_function_callt call(ns.lookup(f_it->first).symbol_expr()); t->make_function_call(call); calls.add_instruction()->make_goto(end.instructions.begin()); goto_programt::targett g=gotos.add_instruction(); diff --git a/src/goto-cc/linker_script_merge.cpp b/src/goto-cc/linker_script_merge.cpp index 7c8b04ac316..9a2acc43520 100644 --- a/src/goto-cc/linker_script_merge.cpp +++ b/src/goto-cc/linker_script_merge.cpp @@ -590,15 +590,13 @@ int linker_script_merget::ls_data2instructions( goto_programt::instructionst initialize_instructions=gp.instructions; for(const auto &d : data["regions"].array) { - code_function_callt f; - const code_typet void_t({}, empty_typet()); - f.function()=symbol_exprt(CPROVER_PREFIX "allocated_memory", void_t); unsigned start=safe_string2unsigned(d["start"].value); unsigned size=safe_string2unsigned(d["size"].value); constant_exprt first=from_integer(start, size_type()); constant_exprt second=from_integer(size, size_type()); - code_function_callt::argumentst args={first, second}; - f.arguments()=args; + const code_typet void_t({}, empty_typet()); + code_function_callt f( + symbol_exprt(CPROVER_PREFIX "allocated_memory", void_t), {first, second}); source_locationt loc; loc.set_file(linker_script); diff --git a/src/goto-instrument/call_sequences.cpp b/src/goto-instrument/call_sequences.cpp index 7138494f2db..74f0687b622 100644 --- a/src/goto-instrument/call_sequences.cpp +++ b/src/goto-instrument/call_sequences.cpp @@ -277,7 +277,7 @@ static void list_calls_and_arguments( if(!i_it->is_function_call()) continue; - const code_function_callt call=to_code_function_call(i_it->code); + const code_function_callt &call = to_code_function_call(i_it->code); const exprt &f=call.function(); diff --git a/src/goto-instrument/function.cpp b/src/goto-instrument/function.cpp index fadf6680b3f..c5066c5e0d9 100644 --- a/src/goto-instrument/function.cpp +++ b/src/goto-instrument/function.cpp @@ -60,7 +60,6 @@ code_function_callt function_to_call( string_constantt function_id_string(argument); code_function_callt call( - nil_exprt(), symbol_exprt(s_it->second.name, s_it->second.type), {typecast_exprt( address_of_exprt( diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp index 7970511b0d4..0ff23583785 100644 --- a/src/goto-instrument/goto_program2code.cpp +++ b/src/goto-instrument/goto_program2code.cpp @@ -1361,16 +1361,11 @@ goto_programt::const_targett goto_program2codet::convert_start_thread( system_headers.insert("pthread.h"); - code_function_callt f; - // we don't bother setting the type - f.lhs()=cf.lhs(); - f.function() = - symbol_exprt("pthread_create", code_typet({}, empty_typet())); const null_pointer_exprt n(pointer_type(empty_typet())); - f.arguments().push_back(n); - f.arguments().push_back(n); - f.arguments().push_back(cf.function()); - f.arguments().push_back(cf.arguments().front()); + code_function_callt f( + cf.lhs(), + symbol_exprt("pthread_create", code_typet({}, empty_typet())), + {n, n, cf.function(), cf.arguments().front()}); dest.move_to_operands(f); return thread_end; diff --git a/src/goto-instrument/interrupt.cpp b/src/goto-instrument/interrupt.cpp index 38863e490fc..f9882332fd5 100644 --- a/src/goto-instrument/interrupt.cpp +++ b/src/goto-instrument/interrupt.cpp @@ -94,9 +94,8 @@ void interrupt( const source_locationt &source_location= original_instruction.source_location; - code_function_callt isr_call; + code_function_callt isr_call(interrupt_handler); isr_call.add_source_location()=source_location; - isr_call.function()=interrupt_handler; goto_programt::targett t_goto=i_it; goto_programt::targett t_call=goto_program.insert_after(t_goto); @@ -127,9 +126,8 @@ void interrupt( const source_locationt &source_location=i_it->source_location; - code_function_callt isr_call; + code_function_callt isr_call(interrupt_handler); isr_call.add_source_location()=source_location; - isr_call.function()=interrupt_handler; t_goto->make_goto(t_orig); t_goto->source_location=source_location; diff --git a/src/goto-instrument/splice_call.cpp b/src/goto-instrument/splice_call.cpp index cf4d33a62f1..a09af770f2c 100644 --- a/src/goto-instrument/splice_call.cpp +++ b/src/goto-instrument/splice_call.cpp @@ -73,9 +73,9 @@ bool splice_call( caller_fun->second.body.instructions.begin(); goto_programt::targett g= caller_fun->second.body.insert_before(start); - code_function_callt splice_call; - splice_call.function()=ns.lookup(callee_fun->first).symbol_expr(); - g->make_function_call(to_code_function_call(splice_call)); + const code_function_callt splice_call( + ns.lookup(callee_fun->first).symbol_expr()); + g->make_function_call(splice_call); // update counters etc. goto_functions.update(); diff --git a/src/goto-instrument/thread_instrumentation.cpp b/src/goto-instrument/thread_instrumentation.cpp index 10c4dfff1f5..35ef72c509c 100644 --- a/src/goto-instrument/thread_instrumentation.cpp +++ b/src/goto-instrument/thread_instrumentation.cpp @@ -104,12 +104,10 @@ void mutex_init_instrumentation( { goto_programt::targett t=goto_program.insert_after(it); - code_function_callt call; - - call.function()=f_it->second.symbol_expr(); - call.arguments().resize(2); - call.arguments()[0]=address_of_exprt(code_assign.lhs()); - call.arguments()[1]=address_of_exprt(string_constantt("mutex-init")); + const code_function_callt call( + f_it->second.symbol_expr(), + {address_of_exprt(code_assign.lhs()), + address_of_exprt(string_constantt("mutex-init"))}); t->make_function_call(call); t->source_location=it->source_location; diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 7fce24e1d24..eadc0ffcf07 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -844,8 +844,7 @@ void goto_convertt::convert_cpp_delete( to_code_type(delete_symbol.type()).parameters().front().type(); code_function_callt delete_call( - nil_exprt(), delete_symbol, {typecast_exprt(tmp_op, arg_type)}); - delete_call.lhs().make_nil(); + delete_symbol, {typecast_exprt(tmp_op, arg_type)}); delete_call.add_source_location()=code.source_location(); convert(delete_call, dest, ID_cpp); diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp index f45a085d007..63537c3d721 100644 --- a/src/goto-programs/goto_convert_side_effect.cpp +++ b/src/goto-programs/goto_convert_side_effect.cpp @@ -344,7 +344,7 @@ void goto_convertt::remove_function_call( if(!result_is_used) { - code_function_callt call(nil_exprt(), expr.op0(), expr.op1().operands()); + code_function_callt call(expr.op0(), expr.op1().operands()); call.add_source_location()=expr.source_location(); convert_function_call(call, dest, mode); expr.make_nil(); diff --git a/src/goto-programs/mm_io.cpp b/src/goto-programs/mm_io.cpp index f6dbcb88041..f0dce34ce36 100644 --- a/src/goto-programs/mm_io.cpp +++ b/src/goto-programs/mm_io.cpp @@ -66,10 +66,9 @@ void mm_io( const typet &pt=ct.parameters()[0].type(); const typet &st=ct.parameters()[1].type(); exprt size=size_of_expr(d.type(), ns); - code_function_callt fc(mm_io_r); - fc.arguments().resize(2); - fc.arguments()[0]=typecast_exprt(d.pointer(), pt); - fc.arguments()[1]=typecast_exprt(size, st); + const code_function_callt fc( + mm_io_r, + {typecast_exprt(d.pointer(), pt), typecast_exprt(size, st)}); goto_function.body.insert_before_swap(it); it->make_function_call(fc); it->source_location=source_location; @@ -90,11 +89,11 @@ void mm_io( const typet &st=ct.parameters()[1].type(); const typet &vt=ct.parameters()[2].type(); exprt size=size_of_expr(d.type(), ns); - code_function_callt fc(mm_io_w); - fc.arguments().resize(3); - fc.arguments()[0]=typecast_exprt(d.pointer(), pt); - fc.arguments()[1]=typecast_exprt(size, st); - fc.arguments()[2]=typecast_exprt(a.rhs(), vt); + const code_function_callt fc( + mm_io_w, + {typecast_exprt(d.pointer(), pt), + typecast_exprt(size, st), + typecast_exprt(a.rhs(), vt)}); goto_function.body.insert_before_swap(it); it->make_function_call(fc); it->source_location=source_location; diff --git a/src/goto-programs/remove_asm.cpp b/src/goto-programs/remove_asm.cpp index cdf36734ff1..ae3eac70747 100644 --- a/src/goto-programs/remove_asm.cpp +++ b/src/goto-programs/remove_asm.cpp @@ -135,9 +135,6 @@ void remove_asmt::msc_asm_function_call( { irep_idt function_identifier = function_base_name; - code_function_callt function_call; - function_call.lhs().make_nil(); - const typet void_pointer = pointer_type(void_typet()); code_typet fkt_type({}, void_typet()); @@ -145,7 +142,7 @@ void remove_asmt::msc_asm_function_call( symbol_exprt fkt(function_identifier, fkt_type); - function_call.function() = fkt; + code_function_callt function_call(fkt); goto_programt::targett call = dest.add_instruction(FUNCTION_CALL); call->code = function_call; diff --git a/src/util/std_code.h b/src/util/std_code.h index 2367849b6ca..53471e791d1 100644 --- a/src/util/std_code.h +++ b/src/util/std_code.h @@ -925,6 +925,18 @@ class code_function_callt:public codet arguments() = _arguments; } + code_function_callt(const exprt &_function, argumentst &&_arguments) + : code_function_callt(_function) + { + arguments() = std::move(_arguments); + } + + code_function_callt(const exprt &_function, const argumentst &_arguments) + : code_function_callt(_function) + { + arguments() = _arguments; + } + exprt &lhs() { return op0(); diff --git a/unit/analyses/call_graph.cpp b/unit/analyses/call_graph.cpp index 753809ac924..f3d9d1eb695 100644 --- a/unit/analyses/call_graph.cpp +++ b/unit/analyses/call_graph.cpp @@ -48,12 +48,9 @@ SCENARIO("call_graph", { code_blockt calls; - code_function_callt call1; - call1.function()=symbol_exprt("A", void_function_type); - code_function_callt call2; - call2.function()=symbol_exprt("B", void_function_type); - code_function_callt call3; - call3.function()=symbol_exprt("B", void_function_type); + code_function_callt call1(symbol_exprt("A", void_function_type)); + code_function_callt call2(symbol_exprt("B", void_function_type)); + code_function_callt call3(symbol_exprt("B", void_function_type)); calls.move_to_operands(call1); calls.move_to_operands(call2); calls.move_to_operands(call3); @@ -64,10 +61,8 @@ SCENARIO("call_graph", { code_blockt calls; - code_function_callt call1; - call1.function()=symbol_exprt("C", void_function_type); - code_function_callt call2; - call2.function()=symbol_exprt("D", void_function_type); + code_function_callt call1(symbol_exprt("C", void_function_type)); + code_function_callt call2(symbol_exprt("D", void_function_type)); calls.move_to_operands(call1); calls.move_to_operands(call2); diff --git a/unit/analyses/dependence_graph.cpp b/unit/analyses/dependence_graph.cpp index 2ccfb017773..c26fcfda0ce 100644 --- a/unit/analyses/dependence_graph.cpp +++ b/unit/analyses/dependence_graph.cpp @@ -76,8 +76,7 @@ SCENARIO("dependence_graph", "[core][analyses][dependence_graph]") from_integer(0, int_type)); code_blockt then_block; - code_function_callt call; - call.function() = symbol_exprt("b", void_function_type); + code_function_callt call(symbol_exprt("b", void_function_type)); then_block.move_to_operands(call); code_assignt assign_x( x_symbol.symbol_expr(), from_integer(1, int_type)); diff --git a/unit/analyses/disconnect_unreachable_nodes_in_graph.cpp b/unit/analyses/disconnect_unreachable_nodes_in_graph.cpp index 729832393c1..5a8cde6def0 100644 --- a/unit/analyses/disconnect_unreachable_nodes_in_graph.cpp +++ b/unit/analyses/disconnect_unreachable_nodes_in_graph.cpp @@ -48,10 +48,8 @@ SCENARIO("graph", "[core][util][graph]") { code_blockt calls; - code_function_callt call1; - call1.function() = symbol_exprt("A", void_function_type); - code_function_callt call2; - call2.function() = symbol_exprt("B", void_function_type); + code_function_callt call1(symbol_exprt("A", void_function_type)); + code_function_callt call2(symbol_exprt("B", void_function_type)); calls.move_to_operands(call1); calls.move_to_operands(call2); @@ -60,10 +58,8 @@ SCENARIO("graph", "[core][util][graph]") { code_blockt calls; - code_function_callt call1; - call1.function() = symbol_exprt("C", void_function_type); - code_function_callt call2; - call2.function() = symbol_exprt("D", void_function_type); + code_function_callt call1(symbol_exprt("C", void_function_type)); + code_function_callt call2(symbol_exprt("D", void_function_type)); calls.move_to_operands(call1); calls.move_to_operands(call2); @@ -72,10 +68,8 @@ SCENARIO("graph", "[core][util][graph]") { code_blockt calls; - code_function_callt call1; - call1.function() = symbol_exprt("F", void_function_type); - code_function_callt call2; - call2.function() = symbol_exprt("G", void_function_type); + code_function_callt call1(symbol_exprt("F", void_function_type)); + code_function_callt call2(symbol_exprt("G", void_function_type)); calls.move_to_operands(call1); calls.move_to_operands(call2);