string_constantt: strengthen typing

1) The string_constantt class is expected to maintain the invariant that its
type is an array type.  This is now made explicit by changing the type of
string_constantt::type().

2) A convenience helper to obtain the character type of the string is added.

Author: kroening

src/util/string_constant.cpp

@@ -12,25 +12,40 @@ Author: Daniel Kroening, [email protected]
 #include "c_types.h"
 #include "std_expr.h"
 
+static array_typet make_type(const irep_idt &value)
+{
+  exprt size_expr = from_integer(value.size() + 1, c_index_type());
+  return array_typet(char_type(), size_expr);
+}
+
 string_constantt::string_constantt(const irep_idt &_value)
-  : nullary_exprt(ID_string_constant, typet())
+  : nullary_exprt(ID_string_constant, make_type(_value))
 {
   set_value(_value);
 }
 
-void string_constantt::set_value(const irep_idt &value)
+void string_constantt::set_value(const irep_idt &_value)
 {
-  exprt size_expr = from_integer(value.size() + 1, c_index_type());
-  type()=array_typet(char_type(), size_expr);
-  set(ID_value, value);
+  exprt::type() = make_type(_value);
+  set(ID_value, _value);
+}
+
+const array_typet &string_constantt::type() const
+{
+  return to_array_type(exprt::type());
+}
+
+array_typet &string_constantt::type()
+{
+  return to_array_type(exprt::type());
 }
 
 /// convert string into array constant
 array_exprt string_constantt::to_array_expr() const
 {
   const std::string &str=get_string(ID_value);
   std::size_t string_size=str.size()+1; // we add the zero
-  const typet &char_type = to_array_type(type()).element_type();
+  const typet &char_type = string_constantt::char_type();
   bool char_is_unsigned=char_type.id()==ID_unsignedbv;
 
   exprt size = from_integer(string_size, c_index_type());

src/util/string_constant.h

@@ -14,16 +14,24 @@ Author: Daniel Kroening, [email protected]
 class string_constantt : public nullary_exprt
 {
 public:
-  explicit string_constantt(const irep_idt &value);
+  explicit string_constantt(const irep_idt &);
 
-  void set_value(const irep_idt &value);
+  void set_value(const irep_idt &);
 
   const irep_idt &get_value() const
   {
     return get(ID_value);
   }
 
   array_exprt to_array_expr() const;
+
+  const typet &char_type() const
+  {
+    return type().element_type();
+  }
+
+  const array_typet &type() const;
+  array_typet &type();
 };
 
 template <>