Merge branch 'master' of https://github.com/diffblue/cbmc

Author: Daniel Kroening

src/ansi-c/expr2c.cpp

@@ -238,6 +238,10 @@ std::string expr2ct::convert_rec(
   {
     return q+"_Bool"+d;
   }
+  else if(src.id()==ID_string)
+  {
+    return q+"__CPROVER_string"+d;
+  }
   else if(src.id()==ID_natural ||
           src.id()==ID_integer ||
           src.id()==ID_rational)

src/linking/zero_initializer.cpp

@@ -267,6 +267,10 @@ exprt zero_initializert::zero_initializer_rec(
 
     return result;
   }
+  else if(type_id==ID_string)
+  {
+    return constant_exprt(irep_idt(), type);
+  }
   else
   {
     err_location(source_location);

src/util/pointer_offset_size.cpp

@@ -222,6 +222,10 @@ mp_integer pointer_offset_bits(
   {
     return 0;
   }
+  else if(type.id()==ID_string)
+  {
+    return config.ansi_c.int_width;
+  }
   else
     return mp_integer(-1);
 }
@@ -479,6 +483,11 @@ exprt size_of_expr(
   {
     return gen_zero(signedbv_typet(config.ansi_c.pointer_width));
   }
+  else if(type.id()==ID_string)
+  {
+    return from_integer(
+      config.ansi_c.int_width, signedbv_typet(config.ansi_c.pointer_width));
+  }
   else
     return nil_exprt();
 }