Cumulative fixup

petr-bauch · petr-bauch · commit 197f23db4374 · 2019-04-23T12:59:47.000+01:00
Will be squashed
diff --git a/regression/snapshot-harness/nondet_initialize_static_arrays/test.desc b/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
diff --git a/regression/snapshot-harness/pointer-function-parameters-struct-mutual-recursion/test.desc b/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
diff --git a/regression/snapshot-harness/pointer-to-array-char/test.desc b/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
diff --git a/regression/snapshot-harness/pointer-to-array-function-parameters-multi-arg-right/test.desc b/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
diff --git a/regression/snapshot-harness/pointer-to-array-int/test.desc b/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
diff --git a/regression/snapshot-harness/pointer_07/test.desc b/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
diff --git a/regression/snapshot-harness/static-array-char/test.desc b/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
diff --git a/src/goto-harness/memory_snapshot_harness_generator.cpp b/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);
   }
diff --git a/src/goto-harness/memory_snapshot_harness_generator_options.h b/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"                   \
diff --git a/src/memory-analyzer/analyze_symbol.cpp b/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);
 
@@ -448,7 +448,7 @@ exprt gdb_value_extractort::get_pointer_value(
     if(target_expr.type() == zero_expr.type())
       return target_expr;
 
-    //otherwise the address of target should type-match
+    // otherwise the address of target should type-match
     const auto result_expr = address_of_exprt(target_expr);
     CHECK_RETURN(result_expr.type() == zero_expr.type());
     return result_expr;
@@ -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;
 }
diff --git a/src/memory-analyzer/gdb_api.cpp b/src/memory-analyzer/gdb_api.cpp
@@ -24,8 +24,8 @@ Author: Malte Mues <mail.mues@gmail.com>
 #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>
 
diff --git a/src/memory-analyzer/gdb_api.h b/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 = "",
diff --git a/src/util/c_types_util.h b/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")
diff --git a/unit/memory-analyzer/gdb_api.cpp b/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")

Original file line number	Diff line number	Diff line change
`@@ -27,7 +27,6 @@ Author: Daniel Poetzl`
`27`	`27`	`#include <linking/static_lifetime_init.h>`
`28`	`28`
`29`	`29`	`#include "goto_harness_generator_factory.h"`
`30`		`-#include <algorithm>`
`31`	`30`
`32`	`31`	`void memory_snapshot_harness_generatort::handle_option(`
`33`	`32`	`const std::string &option,`
`@@ -83,7 +82,7 @@ void memory_snapshot_harness_generatort::handle_option(`
`83`	`82`	`{`
`84`	`83`	`memory_snapshot_file = require_exactly_one_value(option, values);`
`85`	`84`	`}`
`86`		`- else if(option == MEMORY_SNAPSHOT_HARNESS_INITIAL_LOCATION_OPT)`
	`85`	`+ else if(option == MEMORY_SNAPSHOT_HARNESS_INITIAL_GOTO_LOC_OPT)`
`87`	`86`	`{`
`88`	`87`	`initial_goto_location_line = require_exactly_one_value(option, values);`
`89`	`88`	`}`
`@@ -96,7 +95,7 @@ void memory_snapshot_harness_generatort::handle_option(`
`96`	`95`	`variables_to_havoc.insert(candidate);`
`97`	`96`	`}`
`98`	`97`	`}`
`99`		`- else if(option == "initial-source-location")`
	`98`	`+ else if(option == MEMORY_SNAPSHOT_HARNESS_INITIAL_SOURCE_LOC_OPT)`
`100`	`99`	`{`
`101`	`100`	`initial_source_location_line = require_exactly_one_value(option, values);`
`102`	`101`	`}`