Merge pull request #5555 from tautschnig/remove-deprecated-constructors

Remove deprecated function_application_exprt constructor

Author: tautschnig

jbmc/src/java_bytecode/java_utils.cpp

@@ -408,7 +408,7 @@ exprt make_function_application(
     symbol_table);
 
   // Function application
-  return function_application_exprt(symbol.symbol_expr(), arguments, range);
+  return function_application_exprt{symbol.symbol_expr(), arguments};
 }
 
 /// Strip java:: prefix from given identifier

jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp

@@ -20,6 +20,8 @@ Author: Jesse Sigal, [email protected]
 #include <solvers/strings/string_constraint_instantiation.h>
 
 #include <util/config.h>
+#include <util/mathematical_expr.h>
+#include <util/mathematical_types.h>
 #include <util/simplify_expr.h>
 
 /// \class Types used throughout the test. Currently it is impossible to
@@ -203,10 +205,12 @@ SCENARIO(
   GIVEN("The not_contains axioms of String.lastIndexOf(String, Int)")
   {
     // Creating "ab".lastIndexOf("b", 0)
-    const function_application_exprt func(
-      symbol_exprt(ID_cprover_string_last_index_of_func, t.length_type()),
-      {ab, b, from_integer(2)},
-      t.length_type());
+    mathematical_function_typet::domaint domain{
+      {ab.type(), b.type(), t.length_type()}};
+    const function_application_exprt func{
+      symbol_exprt{ID_cprover_string_last_index_of_func,
+                   mathematical_function_typet{domain, t.length_type()}},
+      {ab, b, from_integer(2)}};
 
     // Generating the corresponding axioms and simplifying, recording info
     string_constraint_generatort generator(empty_ns);

jbmc/unit/solvers/strings/string_refinement/dependency_graph.cpp

@@ -11,7 +11,10 @@ Author: Diffblue Ltd.
 
 #include <java_bytecode/java_types.h>
 #include <solvers/strings/string_dependencies.h>
+
 #include <util/arith_tools.h>
+#include <util/mathematical_expr.h>
+#include <util/mathematical_types.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>
 
@@ -55,30 +58,24 @@ SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]")
     const symbol_exprt lhs("lhs", unsignedbv_typet(32));
     const symbol_exprt lhs2("lhs2", unsignedbv_typet(32));
     const symbol_exprt lhs3("lhs3", unsignedbv_typet(32));
-    const java_method_typet fun_type(
-      {java_method_typet::parametert(length_type()),
-       java_method_typet::parametert(pointer_type(java_char_type())),
-       java_method_typet::parametert(string_type),
-       java_method_typet::parametert(string_type)},
+    const mathematical_function_typet fun_type(
+      {length_type(), pointer_type(java_char_type()), string_type, string_type},
       unsignedbv_typet(32));
 
     // fun1 is s3 = s1.concat(s2)
     const function_application_exprt fun1(
       symbol_exprt(ID_cprover_string_concat_func, fun_type),
-      {string3.op0(), string3.op1(), string1, string2},
-      fun_type);
+      {string3.op0(), string3.op1(), string1, string2});
 
     // fun2 is s5 = s3.concat(s4)
     const function_application_exprt fun2(
       symbol_exprt(ID_cprover_string_concat_func, fun_type),
-      {string5.op0(), string5.op1(), string3, string4},
-      fun_type);
+      {string5.op0(), string5.op1(), string3, string4});
 
     // fun3 is s6 = s5.concat(s2)
     const function_application_exprt fun3(
       symbol_exprt(ID_cprover_string_concat_func, fun_type),
-      {string6.op0(), string6.op1(), string5, string2},
-      fun_type);
+      {string6.op0(), string6.op1(), string5, string2});
 
     const equal_exprt equation1(lhs, fun1);
     const equal_exprt equation2(lhs2, fun2);

jbmc/unit/solvers/strings/string_refinement/string_symbol_resolution.cpp

@@ -15,8 +15,11 @@ Author: Diffblue Ltd.
 #include <iostream>
 #include <java_bytecode/java_bytecode_language.h>
 #include <langapi/mode.h>
+
 #include <util/arith_tools.h>
 #include <util/c_types.h>
+#include <util/mathematical_expr.h>
+#include <util/mathematical_types.h>
 #include <util/std_expr.h>
 #include <util/symbol_table.h>
 
@@ -63,11 +66,10 @@ SCENARIO(
 
     WHEN("There is a function call")
     {
-      java_method_typet::parameterst parameters;
-      typet return_type;
+      mathematical_function_typet::domaint domain{{string_typet{}}};
       symbol_exprt fun_sym(
-        "f", java_method_typet(std::move(parameters), return_type));
-      const function_application_exprt fun(fun_sym, {c}, bool_typet());
+        "f", mathematical_function_typet{domain, bool_typet{}});
+      const function_application_exprt fun{fun_sym, {c}};
       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

@@ -19,6 +19,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/expr_initializer.h>
 #include <util/expr_util.h>
 #include <util/mathematical_expr.h>
+#include <util/mathematical_types.h>
 #include <util/pointer_offset_size.h>
 #include <util/prefix.h>
 #include <util/rational.h>
@@ -893,7 +894,14 @@ void goto_convertt::do_function_call_symbol(
     if(lhs.is_nil())
       return;
 
-    const function_application_exprt rhs(function, arguments, lhs.type());
+    const code_typet &function_call_type = to_code_type(function.type());
+    mathematical_function_typet::domaint domain;
+    for(const auto &parameter : function_call_type.parameters())
+      domain.push_back(parameter.type());
+    mathematical_function_typet function_type{domain,
+                                              function_call_type.return_type()};
+    const function_application_exprt rhs(
+      symbol_exprt{function.get_identifier(), function_type}, arguments);
 
     code_assignt assignment(lhs, rhs);
     assignment.add_source_location()=function.source_location();

src/util/mathematical_expr.h

@@ -192,20 +192,6 @@ class function_application_exprt : public binary_exprt
 public:
   using argumentst = exprt::operandst;
 
-  DEPRECATED(
-    SINCE(2019, 3, 3, "use function_application_exprt(fkt, arg) instead"))
-  function_application_exprt(
-    const symbol_exprt &_function,
-    const argumentst &_arguments,
-    const typet &_type)
-    : binary_exprt(
-        _function,
-        ID_function_application,
-        tuple_exprt(_arguments),
-        _type)
-  {
-  }
-
   function_application_exprt(const exprt &_function, argumentst _arguments);
 
   exprt &function()