Remove goto_check_java

The Java front-end instruments checks via other means. The only
remaining use of `goto_check_javat` was handling of the `no-assertions`
and `no-assumptions` command-line options, which is now handled by
`transform_assertions_assumptions`.

Author: tautschnig

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -93,10 +93,6 @@ void janalyzer_parse_optionst::get_command_line_options(optionst &options)
   else
     options.set_option("assumptions", true);
 
-  // magic error label
-  if(cmdline.isset("error-label"))
-    options.set_option("error-label", cmdline.get_values("error-label"));
-
   // Select a specific analysis
   if(cmdline.isset("taint"))
   {
@@ -791,7 +787,8 @@ void janalyzer_parse_optionst::help()
     HELP_SHOW_PROPERTIES
     "\n"
     "Program instrumentation options:\n"
-    HELP_GOTO_CHECK_JAVA
+    " --no-assertions              ignore user assertions\n"
+    " --no-assumptions             ignore user assumptions\n"
     "\n"
     "Other options:\n"
     " --version                    show version and exit\n"

jbmc/src/janalyzer/janalyzer_parse_options.h

@@ -108,11 +108,11 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/show_goto_functions.h>
 #include <goto-programs/show_properties.h>
 
-#include <java_bytecode/goto_check_java.h>
 #include <java_bytecode/java_bytecode_language.h>
 
 class abstract_goto_modelt;
 class ai_baset;
+class goto_functiont;
 class goto_model_functiont;
 class optionst;
 
@@ -127,7 +127,7 @@ class optionst;
   "(little-endian)(big-endian)" \
   OPT_SHOW_GOTO_FUNCTIONS \
   OPT_SHOW_PROPERTIES \
-  OPT_GOTO_CHECK_JAVA \
+  "(no-assertions)(no-assumptions)" \
   "(show-loops)" \
   "(show-symbol-table)(show-parse-tree)" \
   "(show-reachable-properties)(property):" \

jbmc/src/java_bytecode/Makefile

@@ -9,7 +9,6 @@ SRC = assignments_from_json.cpp \
       expr2java.cpp \
       generic_parameter_specialization_map.cpp \
       generic_parameter_specialization_map_keys.cpp \
-      goto_check_java.cpp \
       jar_file.cpp \
       jar_pool.cpp \
       java_bmc_util.cpp \