Constructor for builtin function with no eval

Author: romainbrenguier

src/solvers/refinement/string_builtin_function.cpp

@@ -207,3 +207,32 @@ optionalt<exprt> string_insertion_builtin_functiont::eval(
   const array_typet type(result.type().subtype(), length);
   return make_string(result_value, type);
 }
+
+string_builtin_function_with_no_evalt::string_builtin_function_with_no_evalt(
+  const function_application_exprt &f,
+  array_poolt &array_pool)
+  : function_application(f)
+{
+  const std::vector<exprt> &fun_args = f.arguments();
+  std::size_t i = 0;
+  if(fun_args.size() >= 2 && fun_args[1].type().id() == ID_pointer)
+  {
+    string_res = array_pool.find(fun_args[1], fun_args[0]);
+    i = 2;
+  }
+
+  for(; i < fun_args.size(); ++i)
+  {
+    const auto arg = expr_try_dynamic_cast<struct_exprt>(fun_args[i]);
+    // TODO: use is_refined_string_type ?
+    if(
+      arg && arg->operands().size() == 2 &&
+      arg->op1().type().id() == ID_pointer)
+    {
+      INVARIANT(is_refined_string_type(arg->type()), "should be a string");
+      string_args.push_back(array_pool.find(arg->op1(), arg->op0()));
+    }
+    else
+      args.push_back(fun_args[i]);
+  }
+}

src/solvers/refinement/string_builtin_function.h

@@ -208,6 +208,11 @@ class string_builtin_function_with_no_evalt : public string_builtin_functiont
   optionalt<array_string_exprt> string_res;
   std::vector<array_string_exprt> string_args;
   std::vector<exprt> args;
+
+  string_builtin_function_with_no_evalt(
+    const function_application_exprt &f,
+    array_poolt &array_pool);
+
   std::string name() const override
   {
     return id2string(function_application.id());

src/solvers/refinement/string_refinement_util.cpp

@@ -176,8 +176,8 @@ static std::unique_ptr<string_builtin_functiont> to_string_builtin_function(
                                          : name.get_identifier();
 
   if(id == ID_cprover_string_insert_func)
-    return std::unique_ptr<string_builtin_functiont>(
-      new string_insertion_builtin_functiont(fun_app.arguments(), array_pool));
+    return util_make_unique<string_insertion_builtin_functiont>(
+      fun_app.arguments(), array_pool);
 
   if(id == ID_cprover_string_concat_func)
     return util_make_unique<string_concatenation_builtin_functiont>(