diff --git a/jbmc/src/java_bytecode/java_utils.cpp b/jbmc/src/java_bytecode/java_utils.cpp index d4732d7c39a..1ab219088c3 100644 --- a/jbmc/src/java_bytecode/java_utils.cpp +++ b/jbmc/src/java_bytecode/java_utils.cpp @@ -285,9 +285,7 @@ exprt make_function_application( declare_function(fun_name, type, symbol_table); // Function application - function_application_exprt call(symbol_exprt(fun_name), type); - call.arguments()=arguments; - return call; + return function_application_exprt(symbol_exprt(fun_name), arguments, type); } /// Strip java:: prefix from given identifier diff --git a/jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp b/jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp index c86bca770de..6947f03beb7 100644 --- a/jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp +++ b/jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp @@ -186,10 +186,10 @@ SCENARIO("instantiate_not_contains", GIVEN("The not_contains axioms of String.lastIndexOf(String, Int)") { // Creating "ab".lastIndexOf("b", 0) - function_application_exprt func( - symbol_exprt(ID_cprover_string_last_index_of_func), t.length_type()); - const exprt::operandst args={ab, b, from_integer(2)}; - func.arguments()=args; + const function_application_exprt func( + symbol_exprt(ID_cprover_string_last_index_of_func), + {ab, b, from_integer(2)}, + t.length_type()); // Generating the corresponding axioms and simplifying, recording info symbol_tablet symtab; diff --git a/jbmc/unit/solvers/refinement/string_refinement/dependency_graph.cpp b/jbmc/unit/solvers/refinement/string_refinement/dependency_graph.cpp index 859f95e33af..80f36fd0cd2 100644 --- a/jbmc/unit/solvers/refinement/string_refinement/dependency_graph.cpp +++ b/jbmc/unit/solvers/refinement/string_refinement/dependency_graph.cpp @@ -66,28 +66,22 @@ SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]") unsignedbv_typet(32)); // fun1 is s3 = s1.concat(s2) - function_application_exprt fun1(fun_type); - fun1.function() = symbol_exprt(ID_cprover_string_concat_func); - fun1.arguments().push_back(string3.op0()); - fun1.arguments().push_back(string3.op1()); - fun1.arguments().push_back(string1); - fun1.arguments().push_back(string2); + const function_application_exprt fun1( + symbol_exprt(ID_cprover_string_concat_func), + {string3.op0(), string3.op1(), string1, string2}, + fun_type); // fun2 is s5 = s3.concat(s4) - function_application_exprt fun2(fun_type); - fun2.function() = symbol_exprt(ID_cprover_string_concat_func); - fun2.arguments().push_back(string5.op0()); - fun2.arguments().push_back(string5.op1()); - fun2.arguments().push_back(string3); - fun2.arguments().push_back(string4); + const function_application_exprt fun2( + symbol_exprt(ID_cprover_string_concat_func), + {string5.op0(), string5.op1(), string3, string4}, + fun_type); // fun3 is s6 = s5.concat(s2) - function_application_exprt fun3(fun_type); - fun3.function() = symbol_exprt(ID_cprover_string_concat_func); - fun3.arguments().push_back(string6.op0()); - fun3.arguments().push_back(string6.op1()); - fun3.arguments().push_back(string5); - fun3.arguments().push_back(string2); + const function_application_exprt fun3( + symbol_exprt(ID_cprover_string_concat_func), + {string6.op0(), string6.op1(), string5, string2}, + fun_type); const equal_exprt equation1(lhs, fun1); const equal_exprt equation2(lhs2, fun2); diff --git a/jbmc/unit/solvers/refinement/string_refinement/string_symbol_resolution.cpp b/jbmc/unit/solvers/refinement/string_refinement/string_symbol_resolution.cpp index 443e9126a5f..8b92256c367 100644 --- a/jbmc/unit/solvers/refinement/string_refinement/string_symbol_resolution.cpp +++ b/jbmc/unit/solvers/refinement/string_refinement/string_symbol_resolution.cpp @@ -68,8 +68,7 @@ SCENARIO("string_identifiers_resolution_from_equations", typet return_type; symbol_exprt fun_sym( "f", java_method_typet(std::move(parameters), return_type)); - function_application_exprt fun(fun_sym, bool_typet()); - fun.operands().push_back(c); + const function_application_exprt fun(fun_sym, {c}, bool_typet()); symbol_exprt bool_sym("bool_b", bool_typet()); equations.emplace_back(bool_sym, fun); union_find_replacet symbol_resolve = diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index a019f8b63ac..e295f1aafa5 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -900,11 +900,7 @@ void goto_convertt::do_function_call_symbol( if(lhs.is_nil()) return; - function_application_exprt rhs; - rhs.type()=lhs.type(); - rhs.add_source_location()=function.source_location(); - rhs.function()=function; - rhs.arguments()=arguments; + const function_application_exprt rhs(function, arguments, lhs.type()); code_assignt assignment(lhs, rhs); assignment.add_source_location()=function.source_location(); diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp index d5f1fe1ad2b..da11d72c9b3 100644 --- a/src/solvers/smt2/smt2_parser.cpp +++ b/src/solvers/smt2/smt2_parser.cpp @@ -286,11 +286,6 @@ exprt smt2_parsert::function_application( #if 0 const auto &f = id_map[identifier]; - function_application_exprt result; - - result.function()=symbol_exprt(identifier, f.type); - result.arguments()=op; - // check the arguments if(op.size()!=f.type.variables().size()) { @@ -303,12 +298,12 @@ exprt smt2_parsert::function_application( if(op[i].type() != f.type.variables()[i].type()) { error() << "wrong type for arguments for function" << eom; - return result; + return nil_exprt(); } } - result.type()=f.type.range(); - return result; + return function_application_exprt( + symbol_exprt(identifier, f.type), op, f.type.range()); #endif return nil_exprt(); } @@ -675,12 +670,11 @@ exprt smt2_parsert::function_application() { if(id_it->second.type.id()==ID_mathematical_function) { - function_application_exprt app; - app.function()=symbol_exprt(final_id, id_it->second.type); - app.arguments()=op; - app.type()=to_mathematical_function_type( - id_it->second.type).codomain(); - return app; + return function_application_exprt( + symbol_exprt(final_id, id_it->second.type), + op, + to_mathematical_function_type( + id_it->second.type).codomain()); } else return symbol_exprt(final_id, id_it->second.type); diff --git a/src/util/std_expr.h b/src/util/std_expr.h index d8984c8ec33..0b09e7a3097 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -4333,22 +4333,16 @@ class null_pointer_exprt:public constant_exprt class function_application_exprt:public binary_exprt { public: - function_application_exprt():binary_exprt(ID_function_application) - { - op0()=symbol_exprt(); - } - - explicit function_application_exprt(const typet &_type): - binary_exprt(ID_function_application, _type) - { - op0()=symbol_exprt(); - } + using argumentst = exprt::operandst; function_application_exprt( - const symbol_exprt &_function, const typet &_type): - function_application_exprt(_type) // NOLINT(runtime/explicit) + const symbol_exprt &_function, + const argumentst &_arguments, + const typet &_type) + : binary_exprt(ID_function_application, _type) { function()=_function; + arguments() = _arguments; } symbol_exprt &function() @@ -4361,8 +4355,6 @@ class function_application_exprt:public binary_exprt return static_cast(op0()); } - typedef exprt::operandst argumentst; - argumentst &arguments() { return op1().operands();