Add string_to_upper_case_builtin_functiont constructor

Author: romainbrenguier

src/solvers/refinement/string_builtin_function.cpp

@@ -341,6 +341,14 @@ optionalt<exprt> string_to_upper_case_builtin_functiont::eval(
   return make_string(input_opt.value(), type);
 }
 
+/// Set of constraints ensuring `result` corresponds to `input` in which
+/// lowercase characters of Basic Latin and Latin-1 supplement of unicode
+/// have been converted to uppercase. These constraints are:
+///   1. res.length = str.length && return_code = 0
+///   2. forall i < str.length.
+///        is_lower_case(str[i]) ? res[i] = str[i] - 0x20 : res[i] = str[i]
+///
+/// \param fresh_symbol: generator of fresh symbols
 string_constraintst string_to_upper_case_builtin_functiont::constraints(
   string_constraint_generatort &generator) const
 {

src/solvers/refinement/string_builtin_function.h

@@ -63,8 +63,8 @@ class string_builtin_functiont
   string_builtin_functiont() = default;
 
 protected:
-  explicit string_builtin_functiont(const exprt &return_code)
-    : return_code(return_code)
+  explicit string_builtin_functiont(exprt return_code)
+    : return_code(std::move(return_code))
   {
   }
 };
@@ -76,6 +76,16 @@ class string_transformation_builtin_functiont : public string_builtin_functiont
   array_string_exprt result;
   array_string_exprt input;
 
+  string_transformation_builtin_functiont(
+    exprt return_code,
+    array_string_exprt result,
+    array_string_exprt input)
+    : string_builtin_functiont(std::move(return_code)),
+      result(std::move(result)),
+      input(std::move(result))
+  {
+  }
+
   /// Constructor from arguments of a function application.
   /// The arguments in `fun_args` should be in order:
   /// an integer `result.length`, a character pointer `&result[0]`,