Java front-end: rule out multiple parallel instances of java_bytecode_languaget

jbmc/regression/janalyzer/too-many-args/A.java

@@ -0,0 +1,2 @@
+public class A { }
+class B { }

jbmc/regression/janalyzer/too-many-args/test.desc

@@ -0,0 +1,6 @@
+CORE
+A.class
+B.class
+^Only one \.class, \.jar or \.gbf file should be directly specified on the command-line
+^EXIT=1$
+^SIGNAL=0$

jbmc/regression/jbmc/string_field_aliasing/test.desc

@@ -1,6 +1,6 @@
 CORE
 Cart.class
---cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --trace --java-max-vla-length 96 --java-unwind-enum-static --max-nondet-string-length 200 --unwind 4 Cart.class --function Cart.checkTax4 --string-printable
+--cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --trace --java-max-vla-length 96 --java-unwind-enum-static --max-nondet-string-length 200 --unwind 4 --function Cart.checkTax4 --string-printable
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/jbmc/too-many-args/A.java

@@ -0,0 +1,2 @@
+public class A { }
+class B { }

jbmc/regression/jbmc/too-many-args/test.desc

@@ -0,0 +1,6 @@
+CORE
+A.class
+B.class
+^Only one \.class, \.jar or \.gbf file should be directly specified on the command-line
+^EXIT=6$
+^SIGNAL=0$

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -355,6 +355,17 @@ int janalyzer_parse_optionst::doit()
 
   register_languages();
 
+  if(cmdline.args.size() > 1)
+  {
+    error() << "Only one .class, .jar or .gbf file should be directly "
+      "specified on the command-line. To force loading another another class "
+      "use '--java-load-class somepackage.SomeClass' or "
+      "'--lazy-methods-extra-entry-point somepackage.SomeClass.method' along "
+      "with '--classpath'"
+            << messaget::eom;
+    return CPROVER_EXIT_USAGE_ERROR;
+  }
+
   goto_model =
     initialize_goto_model(cmdline.args, get_message_handler(), options);
 

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -645,6 +645,15 @@ bool java_bytecode_languaget::typecheck(
   const std::string &)
 {
   PRECONDITION(language_options_initialized);
+  // There are various cases in the Java front-end where pre-existing symbols
+  // from a previous load are not handled. We just rule this case out for now;
+  // a user wishing to ensure a particular class is loaded should use
+  // --java-load-class (to force class-loading) or
+  // --lazy-methods-extra-entry-point (to ensure a method body is loaded)
+  // instead of creating two instances of the front-end.
+  INVARIANT(
+    symbol_table.begin() == symbol_table.end(),
+    "the Java front-end should only be used with an empty symbol table");
 
   java_internal_additions(symbol_table);
 

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -530,6 +530,23 @@ int jbmc_parse_optionst::doit()
   stub_objects_are_not_null =
     options.get_bool_option("java-assume-inputs-non-null");
 
+  if(cmdline.args.empty())
+  {
+    error() << "Please provide a program to verify" << eom;
+    return 6;
+  }
+
+  if(cmdline.args.size() != 1)
+  {
+    error() << "Only one .class, .jar or .gbf file should be directly "
+      "specified on the command-line. To force loading another another class "
+      "use '--java-load-class somepackage.SomeClass' or "
+      "'--lazy-methods-extra-entry-point somepackage.SomeClass.method' along "
+      "with '--classpath'"
+            << messaget::eom;
+    return 6;
+  }
+
   if(!cmdline.isset("symex-driven-lazy-loading"))
   {
     std::unique_ptr<goto_modelt> goto_model_ptr;
@@ -716,12 +733,6 @@ int jbmc_parse_optionst::get_goto_program(
   std::unique_ptr<goto_modelt> &goto_model,
   const optionst &options)
 {
-  if(cmdline.args.empty())
-  {
-    error() << "Please provide a program to verify" << eom;
-    return 6;
-  }
-
   {
     lazy_goto_modelt lazy_goto_model=lazy_goto_modelt::from_handler_object(
       *this, options, get_message_handler());