Merge pull request #4943 from peterschrammel/non-existing-entry-point

Error message when entry function body cannot be produced [TG-8299]

Author: peterschrammel

jbmc/regression/jbmc/context-include-exclude/test_excluded_entry_point.desc

@@ -0,0 +1,11 @@
+CORE
+Main.class
+--context-exclude 'org.cprover.MyClass$Inner.' --function 'org.cprover.MyClass$Inner.doIt:(I)I'
+^EXIT=1$
+^SIGNAL=0$
+the program has no entry point
+--
+_Map_base::at
+unordered_map::at: key not found
+--
+Tests that a proper error message is printed.

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -899,6 +899,17 @@ bool java_bytecode_languaget::generate_support_functions(
   // parameter names
   convert_lazy_method(res.main_function.name, symbol_table_builder);
 
+  const symbolt &symbol =
+    symbol_table_builder.lookup_ref(res.main_function.name);
+  if(symbol.value.is_nil())
+  {
+    throw invalid_command_line_argument_exceptiont(
+      "the program has no entry point",
+      "function",
+      "Check that the specified entry point is included by your "
+      "--context-include or --context-exclude options");
+  }
+
   // generate the test harness in __CPROVER__start and a call the entry point
   return java_entry_point(
     symbol_table_builder,