Cumulative fixup

Author: petr-bauch

src/goto-harness/memory_snapshot_harness_generator.cpp

@@ -103,7 +103,12 @@ void memory_snapshot_harness_generatort::handle_option(
   }
   else if(option == MEMORY_SNAPSHOT_HARNESS_HAVOC_VARIABLES_OPT)
   {
-    variables_to_havoc.insert(values.begin(), values.end());
+    std::vector<std::string> havoc_candidates;
+    split_string(values.front(), ',', havoc_candidates, true);
+    for(const auto &candidate : havoc_candidates)
+    {
+      variables_to_havoc.insert(candidate);
+    }
   }
   else
   {

src/memory-analyzer/analyze_symbol.cpp

@@ -190,7 +190,8 @@ exprt symbol_analyzert::get_char_pointer_value(
   }
   else
   {
-    return it->second;
+    return symbol_exprt{to_symbol_expr(it->second).get_identifier(),
+                        expr.type().subtype()};
   }
 }
 
@@ -315,7 +316,14 @@ exprt symbol_analyzert::get_pointer_value(
   {
     if(is_c_char(expr.type().subtype()))
     {
-      return get_char_pointer_value(expr, memory_location, location);
+      INVARIANT(
+        !points_to_member(value),
+        "pointers-to-char shouldn't point to members");
+      const auto result_pointee_expr =
+        get_char_pointer_value(expr, memory_location, location);
+      const auto result_expr = address_of_exprt{result_pointee_expr};
+      CHECK_RETURN(result_expr.type() == zero_expr.type());
+      return result_expr;
     }
     else
     {