Use mode of entry function to generate __CPROVER__start

Previously, when we compiled for instance a C file with no `main()` with goto-cc
it would have no __CPROVER__start. CBMC would use the following logic to
determine the entry point:

1. If `--function` is not passed, use existing `__CPROVER__start`
   -- in our case, we don't have an existing `__CPROVER__start`, so this
      doesn't work for us
2. If `--function` _is_ passed, and a `__CPROVER__start` exists: Generate a new
   entry point calling the passed entry function, based on the mode of the
   existing `__CPROVER__start` (I am not sure why this mode rather than the mode
   of `--function`)
3. Otherwise, iterate over the non-binary input files, determine the language to
   use based on The file extension for each source file, and try to generate an
   appropriate `__CPROVER__start` based on that

The situation of having a single goto-binary with no `__CPROVER__start` as the
input file doesn't fit any of these cases, so regardless of whether `--function`
is passed CBMC is going to fail, complaining that it can't find or generate an
entry point. This adds a fourth case to the list:

4. If `--function` is passed and there is no `__CPROVER__start`, select the
   language based on the mode of the function parameter and use it to generate
   `__CPROVER__start`

This commit doesn't add tests for this change, but
#4014 adds tests that, in the absence of
this change, require hack-y workarounds (such as passing an empty file with a
`.c` extension to force C mode for case 3 in the list above) to work.

Author: hannes-steffenhagen-diffblue

src/goto-programs/initialize_goto_model.cpp

@@ -29,6 +29,32 @@ Author: Daniel Kroening, [email protected]
 #include "goto_convert_functions.h"
 #include "read_goto_binary.h"
 
+/// Generate an entry point that calls a function with the given name, based on
+/// the functions language mode in the symbol table
+static bool generate_entry_point_for_function(
+  const irep_idt &entry_function_name,
+  const optionst &options,
+  goto_modelt &goto_model,
+  message_handlert &message_handler)
+{
+  auto const entry_function_sym =
+    goto_model.symbol_table.lookup(entry_function_name);
+  if(entry_function_sym == nullptr)
+  {
+    throw invalid_command_line_argument_exceptiont{
+      // NOLINTNEXTLINE(whitespace/braces)
+      std::string{"couldn't find function with name `"} +
+        id2string(entry_function_name) + "' in symbol table",
+      "--function"};
+  }
+  PRECONDITION(!entry_function_sym->mode.empty());
+  auto const entry_language = get_language_from_mode(entry_function_sym->mode);
+  CHECK_RETURN(entry_language != nullptr);
+  entry_language->set_message_handler(message_handler);
+  entry_language->set_language_options(options);
+  return entry_language->generate_support_functions(goto_model.symbol_table);
+}
+
 goto_modelt initialize_goto_model(
   const std::vector<std::string> &files,
   message_handlert &message_handler,
@@ -133,10 +159,20 @@ goto_modelt initialize_goto_model(
   }
   else if(!binaries_provided_start)
   {
-    // Allow all language front-ends to try to provide the user-specified
-    // (--function) entry-point, or some language-specific default:
-    entry_point_generation_failed=
-      language_files.generate_support_functions(goto_model.symbol_table);
+    if(options.is_set("function"))
+    {
+      // no entry point is present; Use the mode of the specified entry function
+      // to generate one
+      entry_point_generation_failed = generate_entry_point_for_function(
+        options.get_option("function"), options, goto_model, message_handler);
+    }
+    if(entry_point_generation_failed || !options.is_set("function"))
+    {
+      // Allow all language front-ends to try to provide the user-specified
+      // (--function) entry-point, or some language-specific default:
+      entry_point_generation_failed =
+        language_files.generate_support_functions(goto_model.symbol_table);
+    }
   }
 
   if(entry_point_generation_failed)