Correct refined_string_typet constructor

We make the second argument be the content type. This is more
compatible, and is how it is used at least once in the code base.
The way it was used was inconsistent.

Author: romainbrenguier

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

@@ -36,7 +36,7 @@ class tt
   }
   refined_string_typet string_type() const
   {
-    return refined_string_typet(length_type(), char_type());
+    return refined_string_typet(length_type(), pointer_type(char_type()));
   }
   array_typet witness_type() const
   {

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

@@ -48,7 +48,8 @@ SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]")
   GIVEN("dependency graph")
   {
     string_dependenciest dependencies;
-    refined_string_typet string_type(java_char_type(), java_int_type());
+    const typet string_type =
+      refined_string_typet(java_int_type(), pointer_type(java_char_type()));
     const exprt string1 = make_string_argument("string1");
     const exprt string2 = make_string_argument("string2");
     const exprt string3 = make_string_argument("string3");

src/util/refined_string_type.cpp

@@ -21,10 +21,10 @@ Author: Romain Brenguier, [email protected]
 #include "std_expr.h"
 
 refined_string_typet::refined_string_typet(
-  const typet &index_type, const typet &char_type)
+  const typet &index_type,
+  const typet &content_type)
 {
-  array_typet char_array(char_type, infinity_exprt(index_type));
   components().emplace_back("length", index_type);
-  components().emplace_back("content", char_array);
+  components().emplace_back("content", content_type);
   set_tag(CPROVER_PREFIX"refined_string_type");
 }