Merge pull request diffblue#2473 from tautschnig/vs-update

kroening · web-flow · commit cf797da89260 · 2018-06-26T08:57:43.000+01:00
Remove unused parameter from update_scores
diff --git a/src/cbmc/fault_localization.cpp b/src/cbmc/fault_localization.cpp
@@ -104,8 +104,7 @@ bool fault_localizationt::check(const lpointst &lpoints,
   return true;
 }
 
-void fault_localizationt::update_scores(lpointst &lpoints,
-                                        const lpoints_valuet &value)
+void fault_localizationt::update_scores(lpointst &lpoints)
 {
   for(auto &l : lpoints)
   {
@@ -131,10 +130,10 @@ void fault_localizationt::localize_linear(lpointst &lpoints)
   {
     v[i]=tvt(tvt::tv_enumt::TV_TRUE);
     if(!check(lpoints, v))
-      update_scores(lpoints, v);
+      update_scores(lpoints);
     v[i]=tvt(tvt::tv_enumt::TV_FALSE);
     if(!check(lpoints, v))
-      update_scores(lpoints, v);
+      update_scores(lpoints);
     v[i]=tvt(tvt::tv_enumt::TV_UNKNOWN);
   }
 }
diff --git a/src/cbmc/fault_localization.h b/src/cbmc/fault_localization.h
@@ -72,8 +72,7 @@ class fault_localizationt:
   // specify an lpoint combination to check
   typedef std::vector<tvt> lpoints_valuet;
   bool check(const lpointst &lpoints, const lpoints_valuet &value);
-  void update_scores(lpointst &lpoints,
-                     const lpoints_valuet &value);
+  void update_scores(lpointst &lpoints);
 
   // localization method: flip each point
   void localize_linear(lpointst &lpoints);

Original file line number	Diff line number	Diff line change
`@@ -104,8 +104,7 @@ bool fault_localizationt::check(const lpointst &lpoints,`
`104`	`104`	`return true;`
`105`	`105`	`}`
`106`	`106`
`107`		`-void fault_localizationt::update_scores(lpointst &lpoints,`
`108`		`- const lpoints_valuet &value)`
	`107`	`+void fault_localizationt::update_scores(lpointst &lpoints)`
`109`	`108`	`{`
`110`	`109`	`for(auto &l : lpoints)`
`111`	`110`	`{`
`@@ -131,10 +130,10 @@ void fault_localizationt::localize_linear(lpointst &lpoints)`
`131`	`130`	`{`
`132`	`131`	`v[i]=tvt(tvt::tv_enumt::TV_TRUE);`
`133`	`132`	`if(!check(lpoints, v))`
`134`		`- update_scores(lpoints, v);`
	`133`	`+ update_scores(lpoints);`
`135`	`134`	`v[i]=tvt(tvt::tv_enumt::TV_FALSE);`
`136`	`135`	`if(!check(lpoints, v))`
`137`		`- update_scores(lpoints, v);`
	`136`	`+ update_scores(lpoints);`
`138`	`137`	`v[i]=tvt(tvt::tv_enumt::TV_UNKNOWN);`
`139`	`138`	`}`
`140`	`139`	`}`