Use goto verifier for fault localization in CBMC

Available by using multi-path symex checker

Author: peterschrammel

src/cbmc/cbmc_parse_options.cpp

@@ -34,6 +34,7 @@ Author: Daniel Kroening, [email protected]
 #include <cpp/cprover_library.h>
 
 #include <goto-checker/all_properties_verifier.h>
+#include <goto-checker/all_properties_verifier_with_fault_localization.h>
 #include <goto-checker/all_properties_verifier_with_trace_storage.h>
 #include <goto-checker/bmc_util.h>
 #include <goto-checker/cover_goals_verifier_with_trace_storage.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>
@@ -625,9 +627,19 @@ int cbmc_parse_optionst::doit()
       }
       else
       {
-        verifier =
-          util_make_unique<stop_on_fail_verifiert<multi_path_symex_checkert>>(
-            options, ui_message_handler, goto_model);
+        if(options.get_bool_option("localize-faults"))
+        {
+          verifier =
+            util_make_unique<stop_on_fail_verifier_with_fault_localizationt<
+              multi_path_symex_checkert>>(
+              options, ui_message_handler, goto_model);
+        }
+        else
+        {
+          verifier =
+            util_make_unique<stop_on_fail_verifiert<multi_path_symex_checkert>>(
+              options, ui_message_handler, goto_model);
+        }
       }
     }
     else
@@ -639,8 +651,20 @@ int cbmc_parse_optionst::doit()
       }
       else
       {
-        verifier = util_make_unique<all_properties_verifier_with_trace_storaget<
-          multi_path_symex_checkert>>(options, ui_message_handler, goto_model);
+        if(options.get_bool_option("localize-faults"))
+        {
+          verifier =
+            util_make_unique<all_properties_verifier_with_fault_localizationt<
+              multi_path_symex_checkert>>(
+              options, ui_message_handler, goto_model);
+        }
+        else
+        {
+          verifier =
+            util_make_unique<all_properties_verifier_with_trace_storaget<
+              multi_path_symex_checkert>>(
+              options, ui_message_handler, goto_model);
+        }
       }
     }
   }