Merge pull request #3048 from diffblue/function_application_exprt-constructors

complete constructors for function_application_exprt

Author: tautschnig

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

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;

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);

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 =

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();

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);

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<const symbol_exprt &>(op0());
   }
 
-  typedef exprt::operandst argumentst;
-
   argumentst &arguments()
   {
     return op1().operands();