Make content type an pointer_typet in refined_string_type

Author: romainbrenguier

jbmc/src/java_bytecode/java_string_library_preprocess.h

@@ -37,7 +37,7 @@ class java_string_library_preprocesst:public messaget
   java_string_library_preprocesst()
     : char_type(java_char_type()),
       index_type(java_int_type()),
-      refined_string_type(index_type, char_type)
+      refined_string_type(index_type, pointer_type(char_type))
   {
   }
 

src/util/refined_string_type.cpp

@@ -22,7 +22,7 @@ Author: Romain Brenguier, [email protected]
 
 refined_string_typet::refined_string_typet(
   const typet &index_type,
-  const typet &content_type)
+  const pointer_typet &content_type)
 {
   components().emplace_back("length", index_type);
   components().emplace_back("content", content_type);

src/util/refined_string_type.h

@@ -26,7 +26,9 @@ Author: Romain Brenguier, [email protected]
 class refined_string_typet: public struct_typet
 {
 public:
-  refined_string_typet(const typet &index_type, const typet &char_type);
+  refined_string_typet(
+    const typet &index_type,
+    const pointer_typet &content_type);
 
   // Type for the content (list of characters) of a string
   const array_typet &get_content_type() const

src/util/string_expr.h

@@ -198,7 +198,7 @@ class refined_string_exprt : public struct_exprt,
     : refined_string_exprt(
         _length,
         _content,
-        refined_string_typet(_length.type(), _content.type()))
+        refined_string_typet(_length.type(), to_pointer_type(_content.type())))
   {
   }