Correct refined_string_typet constructor

We make the second argument be a the content type which makes it more
flexible, and is compatible with how it was used once. We 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,9 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 #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");
 }