Fix based on comments

Author: Petr Bauch

src/goto-harness/function_call_harness_generator.cpp

@@ -272,7 +272,9 @@ void function_call_harness_generatort::implt::generate_initialisation_code_for(
   recursive_initialization->initialize(lhs, 0, {}, block);
 }
 
-void function_call_harness_generatort::validate_options()
+
+void function_call_harness_generatort::validate_options(
+  const goto_modelt &goto_model)
 {
   if(p_impl->function == ID_empty)
     throw invalid_command_line_argument_exceptiont{

src/goto-harness/function_call_harness_generator.h

@@ -33,7 +33,7 @@ class function_call_harness_generatort : public goto_harness_generatort
     const std::string &option,
     const std::list<std::string> &values) override;
 
-  void validate_options() override;
+  void validate_options(const goto_modelt &goto_model) override;
 
 private:
   std::size_t require_one_size_value(

src/goto-harness/goto_harness_generator.h

@@ -35,7 +35,7 @@ class goto_harness_generatort
     const std::list<std::string> &values) = 0;
 
   /// Check if options are in a sane state, throw otherwise
-  virtual void validate_options() = 0;
+  virtual void validate_options(const goto_modelt &goto_model) = 0;
 
   /// Returns the only value of a single element list,
   /// throws an exception if not passed a single element list

src/goto-harness/goto_harness_generator_factory.cpp

@@ -31,7 +31,8 @@ void goto_harness_generator_factoryt::register_generator(
 std::unique_ptr<goto_harness_generatort>
 goto_harness_generator_factoryt::factory(
   const std::string &generator_name,
-  const generator_optionst &generator_options)
+  const generator_optionst &generator_options,
+  const goto_modelt &goto_model)
 {
   auto it = generators.find(generator_name);
 
@@ -42,7 +43,7 @@ goto_harness_generator_factoryt::factory(
     {
       generator->handle_option(option.first, option.second);
     }
-    generator->validate_options();
+    generator->validate_options(goto_model);
 
     return generator;
   }

src/goto-harness/goto_harness_generator_factory.h

@@ -48,7 +48,8 @@ class goto_harness_generator_factoryt
   /// throws if no generator with the supplied name is registered.
   std::unique_ptr<goto_harness_generatort> factory(
     const std::string &generator_name,
-    const generator_optionst &generator_options);
+    const generator_optionst &generator_options,
+    const goto_modelt &goto_model);
 
 private:
   std::map<std::string, build_generatort> generators;

src/goto-harness/goto_harness_parse_options.cpp

@@ -50,11 +50,6 @@ int goto_harness_parse_optionst::doit()
 
   auto factory_options = collect_generate_factory_options();
 
-  // Initialise harness generator
-  auto harness_generator =
-    factory.factory(got_harness_config.harness_type, factory_options);
-  CHECK_RETURN(harness_generator != nullptr);
-
   // This just sets up the defaults (and would interpret options such as --32).
   config.set(cmdline);
 
@@ -67,8 +62,28 @@ int goto_harness_parse_optionst::doit()
                                      got_harness_config.in_file + "'"};
   }
   auto goto_model = std::move(read_goto_binary_result.value());
+
+  // This has to be called after the defaults are set up (as per the
+  // config.set(cmdline) above) otherwise, e.g. the architecture specification
+  // will be unknown.
   config.set_from_symbol_table(goto_model.symbol_table);
 
+  if(goto_model.symbol_table.has_symbol(
+       got_harness_config.harness_function_name))
+  {
+    throw invalid_command_line_argument_exceptiont(
+      "harness function `" +
+        id2string(got_harness_config.harness_function_name) +
+        "` already in "
+        "the symbol table",
+      "--" GOTO_HARNESS_GENERATOR_HARNESS_FUNCTION_NAME_OPT);
+  }
+
+  // Initialise harness generator
+  auto harness_generator = factory.factory(
+    got_harness_config.harness_type, factory_options, goto_model);
+  CHECK_RETURN(harness_generator != nullptr);
+
   harness_generator->generate(
     goto_model, got_harness_config.harness_function_name);