Merge pull request #3872 from tautschnig/symbol_exprt-function_application

Use consistent types with function_application_exprt [blocks: #3766]

Author: tautschnig

jbmc/src/java_bytecode/java_utils.cpp

@@ -247,8 +247,9 @@ void java_add_components_to_class(
 /// \param function_name: a name
 /// \param type: a type
 /// \param symbol_table: symbol table
-void declare_function(
-  irep_idt function_name,
+/// \return newly created symbol
+static auxiliary_symbolt declare_function(
+  const irep_idt &function_name,
   const typet &type,
   symbol_table_baset &symbol_table)
 {
@@ -260,6 +261,8 @@ void declare_function(
   func_symbol.name=function_name;
   func_symbol.type=type;
   symbol_table.add(func_symbol);
+
+  return func_symbol;
 }
 
 /// Create a function application expression.
@@ -275,14 +278,11 @@ exprt make_function_application(
   const typet &type,
   symbol_table_baset &symbol_table)
 {
-  // Names of function to call
-  std::string fun_name=id2string(function_name);
-
   // Declaring the function
-  declare_function(fun_name, type, symbol_table);
+  const auto symbol = declare_function(function_name, type, symbol_table);
 
   // Function application
-  return function_application_exprt(symbol_exprt(fun_name), arguments, type);
+  return function_application_exprt(symbol.symbol_expr(), arguments, type);
 }
 
 /// Strip java:: prefix from given identifier

jbmc/src/java_bytecode/java_utils.h

@@ -87,11 +87,6 @@ size_t find_closing_delimiter(
   char open_char,
   char close_char);
 
-void declare_function(
-  irep_idt function_name,
-  const typet &type,
-  symbol_table_baset &symbol_table);
-
 exprt make_function_application(
   const irep_idt &function_name,
   const exprt::operandst &arguments,

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

@@ -194,7 +194,7 @@ SCENARIO(
   {
     // Creating "ab".lastIndexOf("b", 0)
     const function_application_exprt func(
-      symbol_exprt(ID_cprover_string_last_index_of_func),
+      symbol_exprt(ID_cprover_string_last_index_of_func, t.length_type()),
       {ab, b, from_integer(2)},
       t.length_type());
 

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

@@ -64,19 +64,19 @@ SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]")
 
     // fun1 is s3 = s1.concat(s2)
     const function_application_exprt fun1(
-      symbol_exprt(ID_cprover_string_concat_func),
+      symbol_exprt(ID_cprover_string_concat_func, fun_type),
       {string3.op0(), string3.op1(), string1, string2},
       fun_type);
 
     // fun2 is s5 = s3.concat(s4)
     const function_application_exprt fun2(
-      symbol_exprt(ID_cprover_string_concat_func),
+      symbol_exprt(ID_cprover_string_concat_func, fun_type),
       {string5.op0(), string5.op1(), string3, string4},
       fun_type);
 
     // fun3 is s6 = s5.concat(s2)
     const function_application_exprt fun3(
-      symbol_exprt(ID_cprover_string_concat_func),
+      symbol_exprt(ID_cprover_string_concat_func, fun_type),
       {string6.op0(), string6.op1(), string5, string2},
       fun_type);