Use goto verifier for fault localization in CBMC

Available by using multi-path symex checker

Author: peterschrammel

src/cbmc/cbmc_parse_options.cpp

@@ -35,6 +35,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-checker/all_properties_verifier.h>
 #include <goto-checker/all_properties_verifier_with_trace_storage.h>
+#include <goto-checker/all_properties_verifier_with_fault_localization.h>
 #include <goto-checker/bmc_util.h>
 #include <goto-checker/cover_goals_verifier_with_trace_storage.h>
 #include <goto-checker/multi_path_symex_checker.h>
@@ -43,6 +44,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-checker/single_path_symex_checker.h>
 #include <goto-checker/single_path_symex_only_checker.h>
 #include <goto-checker/stop_on_fail_verifier.h>
+#include <goto-checker/stop_on_fail_verifier_with_fault_localization.h>
 
 #include <goto-programs/adjust_float_expressions.h>
 #include <goto-programs/initialize_goto_model.h>
@@ -617,10 +619,11 @@ int cbmc_parse_optionst::doit()
   {
     if(options.get_bool_option("stop-on-fail"))
     {
-      if(options.get_bool_option("paths"))
+      if(options.get_bool_option("localize-faults"))
       {
         verifier =
-          util_make_unique<stop_on_fail_verifiert<single_path_symex_checkert>>(
+          util_make_unique<stop_on_fail_verifier_with_fault_localizationt<
+            multi_path_symex_checkert>>(
             options, ui_message_handler, goto_model);
       }
       else
@@ -632,10 +635,12 @@ int cbmc_parse_optionst::doit()
     }
     else
     {
-      if(options.get_bool_option("paths"))
+      if(options.get_bool_option("localize-faults"))
       {
-        verifier = util_make_unique<all_properties_verifier_with_trace_storaget<
-          single_path_symex_checkert>>(options, ui_message_handler, goto_model);
+        verifier =
+          util_make_unique<all_properties_verifier_with_fault_localizationt<
+            multi_path_symex_checkert>>(
+            options, ui_message_handler, goto_model);
       }
       else
       {