Do not unnecessarily use C string functions

src/goto-programs/interpreter_evaluate.cpp

@@ -389,14 +389,11 @@ void interpretert::evaluate(
     }
     else if(expr.type().id()==ID_string)
     {
-      irep_idt value=to_constant_expr(expr).get_value();
-      const char *str=value.c_str();
-      std::size_t length=strlen(str)+1;
+      const std::string &value = id2string(to_constant_expr(expr).get_value());
       if(show)
         warning() << "string decoding not fully implemented "
-                  << length << eom;
-      mp_integer tmp = get_string_container()[id2string(value)];
-      dest.push_back(tmp);
+                  << value.size() + 1 << eom;
+      dest.push_back(get_string_container()[value]);
       return;
     }
     else

src/goto-programs/string_abstraction.cpp

@@ -11,8 +11,10 @@ Author: Daniel Kroening, [email protected]
 
 #include "string_abstraction.h"
 
-#include <cstring>
+#include <algorithm>
 
+#include <util/arith_tools.h>
+#include <util/c_types.h>
 #include <util/pointer_predicates.h>
 #include <util/std_expr.h>
 #include <util/std_code.h>
@@ -759,7 +761,11 @@ bool string_abstractiont::build(const exprt &object, exprt &dest, bool write)
 
   if(object.id()==ID_string_constant)
   {
-    mp_integer str_len=strlen(object.get(ID_value).c_str());
+    const std::string &str_value = id2string(object.get(ID_value));
+    // make sure we handle the case of a string constant with string-terminating
+    // \0 in it
+    const std::size_t str_len =
+      std::min(str_value.size(), str_value.find('\0'));
     return build_symbol_constant(str_len, str_len+1, dest);
   }