Modify the user option to take file name as well

To prevent the line number occurring in multiple files and us choosing the wrong
initial instruction.

Author: Petr Bauch

regression/goto-harness/havoc-global-int-03/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-line 6 --havoc-variables x
+--harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-file-line main.c:6 --havoc-variables x
 ^EXIT=10$
 ^SIGNAL=0$
 \[main.assertion.1\] line [0-9]+ assertion x == 1: SUCCESS

src/goto-harness/memory_snapshot_harness_generator.cpp

@@ -63,10 +63,23 @@ void memory_snapshot_harness_generatort::handle_option(
   {
     variables_to_havoc.insert(values.begin(), values.end());
   }
-  else if(option == "initial-line")
+  else if(option == "initial-file-line")
   {
-    const std::string initial_line = require_exactly_one_value(option, values);
-    line_number = optionalt<unsigned>(safe_string2unsigned(initial_line));
+    const std::string initial_file_line =
+      require_exactly_one_value(option, values);
+
+    std::vector<std::string> start;
+    split_string(initial_file_line, ':', start, true);
+
+    if(start.size() != 2 || start.front().empty() || start.back().empty())
+    {
+      throw invalid_command_line_argument_exceptiont(
+        "invalid initial location specification", "--initial-file-line");
+    }
+
+    initial_file_name = start.front();
+    initial_line_number =
+      optionalt<unsigned>(safe_string2unsigned(start.back()));
   }
   else
   {
@@ -81,7 +94,7 @@ memory_snapshot_harness_generatort::get_start_instruction(
   const goto_modelt &goto_model)
 {
   const auto &goto_functions = goto_model.goto_functions;
-  if(line_number.has_value())
+  if(initial_line_number.has_value())
   {
     // by line: iterate over all instructions until source location match
     for(const auto &entry : goto_functions.function_map)
@@ -96,8 +109,10 @@ memory_snapshot_harness_generatort::get_start_instruction(
         goto_program.instructions.begin(),
         goto_program.instructions.end(),
         [this](const goto_programt::instructiont &instruction) {
-          return safe_string2unsigned(id2string(
-                   instruction.source_location.get_line())) >= *line_number;
+          return instruction.source_location.get_file() == initial_file_name &&
+                 safe_string2unsigned(
+                   id2string(instruction.source_location.get_line())) >=
+                   *initial_line_number;
         });
 
       if(it != goto_program.instructions.end())

src/goto-harness/memory_snapshot_harness_generator.h

@@ -23,7 +23,7 @@ Author: Daniel Poetzl
 #define MEMORY_SNAPSHOT_HARNESS_GENERATOR_OPTIONS                              \
   "(memory-snapshot):"                                                         \
   "(initial-location):"                                                        \
-  "(initial-line):"                                                            \
+  "(initial-file-line):"                                                       \
   "(havoc-variables):" // MEMORY_SNAPSHOT_HARNESS_GENERATOR_OPTIONS
 // clang-format on
 
@@ -35,7 +35,7 @@ Author: Daniel Poetzl
   "--initial-location <func[:<n>]>\n"                                          \
   "                              use given function and location number as "   \
   "entry\n                              point\n"                               \
-  "--initial-line <n>            use given line as entry point\n"              \
+  "--initial-file-line <file:n>  use given file and line as entry point\n"     \
   "--havoc-variables vars        initialise variables from vars to\n"          \
   "                              non-deterministic values"                     \
   // MEMORY_SNAPSHOT_HARNESS_GENERATOR_HELP
@@ -156,7 +156,9 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort
   irep_idt entry_function_name;
   optionalt<unsigned> location_number;
   std::unordered_set<irep_idt> variables_to_havoc;
-  optionalt<unsigned> line_number;
+  irep_idt initial_file_name;
+  optionalt<unsigned> initial_line_number;
+
   optionalt<goto_programt::const_targett> start_instruction;
 
   symbol_exprt func_init_done_var;