Use goto verifier for program-only and show-vcc in JBMC

Author: peterschrammel

jbmc/src/java_bytecode/module_dependencies.txt

@@ -1,5 +1,6 @@
 analyses
 ansi-c # should go away
+goto-checker
 goto-programs
 java_bytecode
 json

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -27,6 +27,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <ansi-c/ansi_c_language.h>
 
+#include <goto-checker/all_properties_verifier.h>
+
 #include <goto-programs/adjust_float_expressions.h>
 #include <goto-programs/lazy_goto_model.h>
 #include <goto-programs/instrument_preconditions.h>
@@ -60,6 +62,7 @@ Author: Daniel Kroening, [email protected]
 #include <java_bytecode/convert_java_nondet.h>
 #include <java_bytecode/java_bytecode_language.h>
 #include <java_bytecode/java_enum_static_init_unwind_handler.h>
+#include <java_bytecode/java_multi_path_symex_only_checker.h>
 #include <java_bytecode/remove_exceptions.h>
 #include <java_bytecode/remove_instanceof.h>
 #include <java_bytecode/remove_java_new.h>
@@ -563,6 +566,19 @@ int jbmc_parse_optionst::doit()
       goto_model.validate(validation_modet::INVARIANT);
     }
 
+    if(
+      options.get_bool_option("program-only") ||
+      options.get_bool_option("show-vcc"))
+    {
+      if(!options.get_bool_option("paths"))
+      {
+        all_properties_verifiert<java_multi_path_symex_only_checkert> verifier(
+          options, ui_message_handler, goto_model);
+        (void)verifier();
+        return CPROVER_EXIT_SUCCESS;
+      }
+    }
+
     // The `configure_bmc` callback passed will enable enum-unwind-static if
     // applicable.
     return bmct::do_language_agnostic_bmc(