Cumulative fixup

Will be squashed.

Author: petr-bauch

regression/snapshot-harness/nondet_initialize_static_arrays/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-p --harness-type initialise-with-memory-snapshot --initial-location main:4 --min-null-tree-depth 10 --max-nondet-tree-depth 4 --havoc-variables p
+p --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 --min-null-tree-depth 10 --max-nondet-tree-depth 4 --havoc-variables p
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL

regression/snapshot-harness/pointer-function-parameters-struct-mutual-recursion/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-p --harness-type initialise-with-memory-snapshot --initial-location main:4 --havoc-variables p --min-null-tree-depth 10 --max-nondet-tree-depth 3
+p --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 --havoc-variables p --min-null-tree-depth 10 --max-nondet-tree-depth 3
 ^SIGNAL=0$
 ^EXIT=0$
 VERIFICATION SUCCESSFUL

regression/snapshot-harness/pointer-to-array-char/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-first,second,array_size --harness-type initialise-with-memory-snapshot --initial-location main:4
+first,second,array_size --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
 ^SIGNAL=0$
 ^EXIT=0$
 VERIFICATION SUCCESSFUL

regression/snapshot-harness/pointer-to-array-function-parameters-multi-arg-right/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-first,second,string_size,prefix,prefix_size --harness-type initialise-with-memory-snapshot --initial-location main:4 --havoc-variables prefix,prefix_size --size-of-array prefix:prefix_size --max-array-size 5
+first,second,string_size,prefix,prefix_size --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 --havoc-variables prefix,prefix_size --size-of-array prefix:prefix_size --max-array-size 5
 ^SIGNAL=0$
 ^EXIT=0$
 VERIFICATION SUCCESSFUL

regression/snapshot-harness/pointer-to-array-int/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-first,second,array_size,prefix,prefix_size --harness-type initialise-with-memory-snapshot --initial-location main:4 --havoc-variables prefix --size-of-array prefix:prefix_size --max-array-size 4
+first,second,array_size,prefix,prefix_size --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 --havoc-variables prefix --size-of-array prefix:prefix_size --max-array-size 4
 ^SIGNAL=0$
 ^EXIT=0$
 VERIFICATION SUCCESSFUL

regression/snapshot-harness/pointer_07/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-p1 --harness-type initialise-with-memory-snapshot --initial-location main:4
+p1 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=10$
 ^SIGNAL=0$
 \[main.assertion.1\] line [0-9]+ assertion p1\[0\] == 1: SUCCESS

regression/snapshot-harness/static-array-char/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-tmp,first,second,array_size --harness-type initialise-with-memory-snapshot --initial-location main:4
+tmp,first,second,array_size --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
 ^SIGNAL=0$
 ^EXIT=0$
 VERIFICATION SUCCESSFUL

src/goto-harness/memory_snapshot_harness_generator.cpp

@@ -27,7 +27,6 @@ Author: Daniel Poetzl
 #include <linking/static_lifetime_init.h>
 
 #include "goto_harness_generator_factory.h"
-#include <algorithm>
 
 void memory_snapshot_harness_generatort::handle_option(
   const std::string &option,
@@ -83,7 +82,7 @@ void memory_snapshot_harness_generatort::handle_option(
   {
     memory_snapshot_file = require_exactly_one_value(option, values);
   }
-  else if(option == MEMORY_SNAPSHOT_HARNESS_INITIAL_LOCATION_OPT)
+  else if(option == MEMORY_SNAPSHOT_HARNESS_INITIAL_GOTO_LOC_OPT)
   {
     initial_goto_location_line = require_exactly_one_value(option, values);
   }
@@ -96,7 +95,7 @@ void memory_snapshot_harness_generatort::handle_option(
       variables_to_havoc.insert(candidate);
     }
   }
-  else if(option == "initial-source-location")
+  else if(option == MEMORY_SNAPSHOT_HARNESS_INITIAL_SOURCE_LOC_OPT)
   {
     initial_source_location_line = require_exactly_one_value(option, values);
   }

src/goto-harness/memory_snapshot_harness_generator_options.h

@@ -12,15 +12,17 @@ Author: Diffblue Ltd.
 #include "common_harness_generator_options.h"
 
 #define MEMORY_SNAPSHOT_HARNESS_SNAPSHOT_OPT "memory-snapshot"
-#define MEMORY_SNAPSHOT_HARNESS_INITIAL_LOCATION_OPT "initial-location"
+#define MEMORY_SNAPSHOT_HARNESS_INITIAL_GOTO_LOC_OPT "initial-goto-location"
+#define MEMORY_SNAPSHOT_HARNESS_INITIAL_SOURCE_LOC_OPT "initial-source-location"
 #define MEMORY_SNAPSHOT_HARNESS_HAVOC_VARIABLES_OPT "havoc-variables"
 #define MEMORY_SNAPSHOT_HARNESS_TREAT_POINTER_AS_ARRAY_OPT "pointer-as-array"
 #define MEMORY_SNAPSHOT_HARNESS_ASSOCIATED_ARRAY_SIZE_OPT "size-of-array"
 
 // clang-format off
 #define MEMORY_SNAPSHOT_HARNESS_GENERATOR_OPTIONS                              \
   "(" MEMORY_SNAPSHOT_HARNESS_SNAPSHOT_OPT "):"                                \
-  "(" MEMORY_SNAPSHOT_HARNESS_INITIAL_LOCATION_OPT "):"                        \
+  "(" MEMORY_SNAPSHOT_HARNESS_INITIAL_GOTO_LOC_OPT "):"                        \
+  "(" MEMORY_SNAPSHOT_HARNESS_INITIAL_SOURCE_LOC_OPT "):"                      \
   "(" MEMORY_SNAPSHOT_HARNESS_HAVOC_VARIABLES_OPT "):"                         \
   "(" MEMORY_SNAPSHOT_HARNESS_TREAT_POINTER_AS_ARRAY_OPT "):"                  \
   "(" MEMORY_SNAPSHOT_HARNESS_ASSOCIATED_ARRAY_SIZE_OPT "):"                   \
@@ -34,9 +36,12 @@ Author: Diffblue Ltd.
   "  initialise-from-memory-snapshot)\n\n"                                     \
   "--" MEMORY_SNAPSHOT_HARNESS_SNAPSHOT_OPT " <file>      initialise memory "  \
   "from JSON memory snapshot\n"                                                \
-  "--" MEMORY_SNAPSHOT_HARNESS_INITIAL_LOCATION_OPT " <func[:<n>]>\n"          \
+  "--" MEMORY_SNAPSHOT_HARNESS_INITIAL_GOTO_LOC_OPT " <func[:<n>]>\n"          \
   "                              use given function and location number as "   \
   "entry\n                              point\n"                               \
+  "--" MEMORY_SNAPSHOT_HARNESS_INITIAL_SOURCE_LOC_OPT " <file:<n>>\n"          \
+  "                              use given file name and line number as "      \
+  "entry\n                              point\n"                               \
   "--" MEMORY_SNAPSHOT_HARNESS_HAVOC_VARIABLES_OPT " vars        initialise"   \
   " variables from `vars' to\n"                                                \
   "                              non-deterministic values\n"                   \

src/memory-analyzer/analyze_symbol.cpp

@@ -420,7 +420,7 @@ exprt gdb_value_extractort::get_pointer_value(
 
     // non-member: split for char/non-char
     const auto target_expr =
-      is_c_char(expr.type().subtype())
+      is_c_char_type(expr.type().subtype())
         ? get_char_pointer_value(expr, memory_location, location)
         : get_non_char_pointer_value(expr, memory_location, location);
 
@@ -528,7 +528,7 @@ exprt gdb_value_extractort::get_expr_value(
       return zero_expr;
     const std::string value = *maybe_value;
 
-    return from_c_boolean_value(value, type);
+    return from_c_boolean_value(id2boolean(value), type);
   }
   else if(type.id() == ID_c_enum)
   {
@@ -640,5 +640,8 @@ void gdb_value_extractort::process_outstanding_assignments()
 
 std::string gdb_value_extractort::get_gdb_value(const exprt &expr)
 {
-  return gdb_api.get_value(c_converter.convert(expr));
+  std::string c_expr = c_converter.convert(expr);
+  const auto maybe_value = gdb_api.get_value(c_expr);
+  CHECK_RETURN(maybe_value.has_value());
+  return *maybe_value;
 }

src/memory-analyzer/gdb_api.cpp

@@ -24,8 +24,8 @@ Author: Malte Mues <[email protected]>
 #include <goto-programs/goto_model.h>
 
 #include <util/prefix.h>
-#include <util/string_utils.h>
 #include <util/string2int.h>
+#include <util/string_utils.h>
 
 #include <sys/wait.h>
 

src/memory-analyzer/gdb_api.h

@@ -67,7 +67,6 @@ class gdb_apit
 
   struct pointer_valuet
   {
-    pointer_valuet() = delete;
     pointer_valuet(
       const std::string &address = "",
       const std::string &pointee = "",

src/util/c_types_util.h

@@ -100,9 +100,9 @@ constant_exprt convert_member_name_to_enum_value(
 /// Convert id to a Boolean value
 /// \param bool_value: A string that is compared to "true" ignoring case.
 /// \return a constant of type Boolean
-bool id2boolean(const irep_idt &bool_value)
+bool id2boolean(const std::string &bool_value)
 {
-  std::string string_value = id2string(bool_value);
+  std::string string_value = bool_value;
   std::transform(
     string_value.begin(), string_value.end(), string_value.begin(), ::tolower);
   if(string_value == "true")

unit/memory-analyzer/gdb_api.cpp

@@ -167,9 +167,16 @@ TEST_CASE("gdb api test", "[core][memory-analyzer]")
     const bool r = gdb_api.run_gdb_to_breakpoint("checkpoint");
     REQUIRE(r);
 
-    REQUIRE(gdb_api.get_value("x") == "8");
-    REQUIRE(gdb_api.get_value("y") == "2.5");
-    REQUIRE(gdb_api.get_value("z") == "c");
+    const auto &x_value = gdb_api.get_value("x");
+    const auto &y_value = gdb_api.get_value("y");
+    const auto &z_value = gdb_api.get_value("z");
+
+    REQUIRE(x_value.has_value());
+    REQUIRE(*x_value == "8");
+    REQUIRE(y_value.has_value());
+    REQUIRE(*y_value == "2.5");
+    REQUIRE(z_value.has_value());
+    REQUIRE(*z_value == "c");
   }
 
   SECTION("query pointers")