Use goto verifier for --paths in JBMC

We can now use single_path_symex_checkert instead of bmct.

Author: peterschrammel

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -66,6 +66,8 @@ Author: Daniel Kroening, [email protected]
 #include <java_bytecode/java_enum_static_init_unwind_handler.h>
 #include <java_bytecode/java_multi_path_symex_checker.h>
 #include <java_bytecode/java_multi_path_symex_only_checker.h>
+#include <java_bytecode/java_single_path_symex_checker.h>
+#include <java_bytecode/java_single_path_symex_only_checker.h>
 #include <java_bytecode/remove_exceptions.h>
 #include <java_bytecode/remove_instanceof.h>
 #include <java_bytecode/remove_java_new.h>
@@ -559,46 +561,83 @@ int jbmc_parse_optionst::doit()
       options.get_bool_option("program-only") ||
       options.get_bool_option("show-vcc"))
     {
-      if(!options.get_bool_option("paths"))
+      std::unique_ptr<goto_verifiert> verifier;
+      if(options.get_bool_option("paths"))
       {
-        all_properties_verifiert<java_multi_path_symex_only_checkert> verifier(
+        verifier = util_make_unique<
+          all_properties_verifiert<java_single_path_symex_only_checkert>>(
+          options, ui_message_handler, goto_model);
+      }
+      else
+      {
+        verifier = util_make_unique<
+          all_properties_verifiert<java_multi_path_symex_only_checkert>>(
           options, ui_message_handler, goto_model);
-        (void)verifier();
-        return CPROVER_EXIT_SUCCESS;
       }
+
+      (void)(*verifier)();
+      return CPROVER_EXIT_SUCCESS;
     }
 
     if(
       options.get_bool_option("dimacs") ||
       !options.get_option("outfile").empty())
     {
-      if(!options.get_bool_option("paths"))
+      std::unique_ptr<goto_verifiert> verifier;
+      if(options.get_bool_option("paths"))
       {
-        stop_on_fail_verifiert<multi_path_symex_checkert> verifier(
+        verifier = util_make_unique<
+          stop_on_fail_verifiert<java_single_path_symex_checkert>>(
           options, ui_message_handler, goto_model);
-        (void)verifier();
-        return CPROVER_EXIT_SUCCESS;
       }
+      else
+      {
+        verifier = util_make_unique<
+          stop_on_fail_verifiert<java_multi_path_symex_checkert>>(
+          options, ui_message_handler, goto_model);
+      }
+
+      (void)(*verifier)();
+      return CPROVER_EXIT_SUCCESS;
     }
 
     std::unique_ptr<goto_verifiert> verifier = nullptr;
 
     if(
-      !options.get_bool_option("paths") && !options.is_set("cover") &&
-      !options.get_bool_option("dimacs") &&
+      !options.is_set("cover") && !options.get_bool_option("dimacs") &&
       options.get_option("outfile").empty())
     {
       if(options.get_bool_option("stop-on-fail"))
       {
-        verifier = util_make_unique<
-          stop_on_fail_verifiert<java_multi_path_symex_checkert>>(
-          options, ui_message_handler, goto_model);
+        if(options.get_bool_option("paths"))
+        {
+          verifier = util_make_unique<
+            stop_on_fail_verifiert<java_single_path_symex_checkert>>(
+            options, ui_message_handler, goto_model);
+        }
+        else
+        {
+          verifier = util_make_unique<
+            stop_on_fail_verifiert<java_multi_path_symex_checkert>>(
+            options, ui_message_handler, goto_model);
+        }
       }
       else
       {
-        verifier = util_make_unique<all_properties_verifier_with_trace_storaget<
-          java_multi_path_symex_checkert>>(
-          options, ui_message_handler, goto_model);
+        if(options.get_bool_option("paths"))
+        {
+          verifier =
+            util_make_unique<all_properties_verifier_with_trace_storaget<
+              java_single_path_symex_checkert>>(
+              options, ui_message_handler, goto_model);
+        }
+        else
+        {
+          verifier =
+            util_make_unique<all_properties_verifier_with_trace_storaget<
+              java_multi_path_symex_checkert>>(
+              options, ui_message_handler, goto_model);
+        }
       }
     }