Merge pull request diffblue#2476 from tautschnig/vs-cex

Daniel Kroening · web-flow · commit c07a09bb0cd3 · 2018-06-26T08:56:06.000+01:00
Remove unused parameter in counterexample beautification
diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
@@ -525,7 +525,7 @@ safety_checkert::resultt bmct::stop_on_fail(prop_convt &prop_conv)
     {
       if(options.get_bool_option("beautify"))
         counterexample_beautificationt()(
-          dynamic_cast<bv_cbmct &>(prop_conv), equation, ns);
+          dynamic_cast<bv_cbmct &>(prop_conv), equation);
 
       error_trace();
       output_graphml(resultt::UNSAFE);
diff --git a/src/cbmc/counterexample_beautification.cpp b/src/cbmc/counterexample_beautification.cpp
@@ -80,8 +80,7 @@ counterexample_beautificationt::get_failed_property(
 
 void counterexample_beautificationt::operator()(
   bv_cbmct &bv_cbmc,
-  const symex_target_equationt &equation,
-  const namespacet &ns)
+  const symex_target_equationt &equation)
 {
   // find failed property
 
diff --git a/src/cbmc/counterexample_beautification.h b/src/cbmc/counterexample_beautification.h
@@ -29,8 +29,7 @@ class counterexample_beautificationt
 
   void operator()(
     bv_cbmct &bv_cbmc,
-    const symex_target_equationt &equation,
-    const namespacet &ns);
+    const symex_target_equationt &equation);
 
 protected:
   void get_minimization_list(
diff --git a/src/cbmc/fault_localization.cpp b/src/cbmc/fault_localization.cpp
@@ -281,7 +281,7 @@ safety_checkert::resultt fault_localizationt::stop_on_fail()
     {
       if(options.get_bool_option("beautify"))
         counterexample_beautificationt()(
-          dynamic_cast<bv_cbmct &>(bmc.prop_conv), bmc.equation, bmc.ns);
+          dynamic_cast<bv_cbmct &>(bmc.prop_conv), bmc.equation);
 
       bmc.error_trace();
     }

Original file line number	Diff line number	Diff line change
`@@ -525,7 +525,7 @@ safety_checkert::resultt bmct::stop_on_fail(prop_convt &prop_conv)`
`525`	`525`	`{`
`526`	`526`	`if(options.get_bool_option("beautify"))`
`527`	`527`	`counterexample_beautificationt()(`
`528`		`- dynamic_cast<bv_cbmct &>(prop_conv), equation, ns);`
	`528`	`+ dynamic_cast<bv_cbmct &>(prop_conv), equation);`
`529`	`529`
`530`	`530`	`error_trace();`
`531`	`531`	`output_graphml(resultt::UNSAFE);`
Original file line number	Diff line number	Diff line change
`@@ -80,8 +80,7 @@ counterexample_beautificationt::get_failed_property(`
`80`	`80`
`81`	`81`	`void counterexample_beautificationt::operator()(`
`82`	`82`	`bv_cbmct &bv_cbmc,`
`83`		`- const symex_target_equationt &equation,`
`84`		`- const namespacet &ns)`
	`83`	`+ const symex_target_equationt &equation)`
`85`	`84`	`{`
`86`	`85`	`// find failed property`
`87`	`86`
Original file line number	Diff line number	Diff line change
`@@ -281,7 +281,7 @@ safety_checkert::resultt fault_localizationt::stop_on_fail()`
`281`	`281`	`{`
`282`	`282`	`if(options.get_bool_option("beautify"))`
`283`	`283`	`counterexample_beautificationt()(`
`284`		`- dynamic_cast<bv_cbmct &>(bmc.prop_conv), bmc.equation, bmc.ns);`
	`284`	`+ dynamic_cast<bv_cbmct &>(bmc.prop_conv), bmc.equation);`
`285`	`285`
`286`	`286`	`bmc.error_trace();`
`287`	`287`	`}`