use apply in cover_util

This avoids the case split over the instruction type.

Author: Daniel Kroening

regression/cbmc-cover/mcdc1/test.desc

@@ -3,12 +3,12 @@ main.c
 --cover mcdc
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.coverage.1\] file main.c line 14 function main MC/DC independence condition `C && D && !E && A && !B.*: SATISFIED$
-^\[main.coverage.2\] file main.c line 14 function main MC/DC independence condition `C && !D && E && A && !B.*: SATISFIED$
-^\[main.coverage.3\] file main.c line 14 function main MC/DC independence condition `!C && D && E && A && !B.*: SATISFIED$
-^\[main.coverage.4\] file main.c line 14 function main MC/DC independence condition `C && D && E && A && !B.*: SATISFIED$
-^\[main.coverage.5\] file main.c line 14 function main MC/DC independence condition `C && D && E && !A && B.*: SATISFIED$
-^\[main.coverage.6\] file main.c line 14 function main MC/DC independence condition `C && D && E && !A && !B.*: SATISFIED$
+^\[main.coverage.\d+\] file main.c line 14 function main MC/DC independence condition `C && D && !E && A && !B.*: SATISFIED$
+^\[main.coverage.\d+\] file main.c line 14 function main MC/DC independence condition `C && !D && E && A && !B.*: SATISFIED$
+^\[main.coverage.\d+\] file main.c line 14 function main MC/DC independence condition `!C && D && E && A && !B.*: SATISFIED$
+^\[main.coverage.\d+\] file main.c line 14 function main MC/DC independence condition `C && D && E && A && !B.*: SATISFIED$
+^\[main.coverage.\d+\] file main.c line 14 function main MC/DC independence condition `C && D && E && !A && B.*: SATISFIED$
+^\[main.coverage.\d+\] file main.c line 14 function main MC/DC independence condition `C && D && E && !A && !B.*: SATISFIED$
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring

regression/cbmc-cover/mcdc2/test.desc

@@ -3,10 +3,10 @@ main.c
 --cover mcdc
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.coverage.1\] file main.c line 10 function main MC/DC independence condition `A && !B && !C.*: SATISFIED$
-^\[main.coverage.2\] file main.c line 10 function main MC/DC independence condition `!A && B && !C.*: SATISFIED$
-^\[main.coverage.3\] file main.c line 10 function main MC/DC independence condition `!A && !B && C.*: SATISFIED$
-^\[main.coverage.4\] file main.c line 10 function main MC/DC independence condition `!A && !B && !C.*: SATISFIED$
+^\[main.coverage.\d+\] file main.c line 10 function main MC/DC independence condition `A && !B && !C.*: SATISFIED$
+^\[main.coverage.\d+\] file main.c line 10 function main MC/DC independence condition `!A && B && !C.*: SATISFIED$
+^\[main.coverage.\d+\] file main.c line 10 function main MC/DC independence condition `!A && !B && C.*: SATISFIED$
+^\[main.coverage.\d+\] file main.c line 10 function main MC/DC independence condition `!A && !B && !C.*: SATISFIED$
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring

regression/cbmc-cover/mcdc4/test.desc

@@ -3,11 +3,11 @@ main.c
 --cover mcdc
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.coverage.1\] file main.c line 11 function main MC/DC independence condition `A && B && C && !D.*: SATISFIED$
-^\[main.coverage.2\] file main.c line 11 function main MC/DC independence condition `A && !B && C && D.*: SATISFIED$
-^\[main.coverage.3\] file main.c line 11 function main MC/DC independence condition `A && !B && C && !D.*: SATISFIED$
-^\[main.coverage.4\] file main.c line 11 function main MC/DC independence condition `!C && D && A && !B.*: SATISFIED$
-^\[main.coverage.5\] file main.c line 11 function main MC/DC independence condition `!A && B && C && !D.*: SATISFIED$
+^\[main.coverage.\d+\] file main.c line 11 function main MC/DC independence condition `A && B && C && !D.*: SATISFIED$
+^\[main.coverage.\d+\] file main.c line 11 function main MC/DC independence condition `A && !B && C && D.*: SATISFIED$
+^\[main.coverage.\d+\] file main.c line 11 function main MC/DC independence condition `A && !B && C && !D.*: SATISFIED$
+^\[main.coverage.\d+\] file main.c line 11 function main MC/DC independence condition `!C && D && A && !B.*: SATISFIED$
+^\[main.coverage.\d+\] file main.c line 11 function main MC/DC independence condition `!A && B && C && !D.*: SATISFIED$
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring

regression/cbmc-cover/mcdc5/test.desc

@@ -3,11 +3,11 @@ main.c
 --cover mcdc
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.coverage.1\] file main.c line 10 function main MC/DC independence condition `A && !B && C && !D.*: SATISFIED$
-^\[main.coverage.2\] file main.c line 10 function main MC/DC independence condition `!C && D && A && !B.*: SATISFIED$
-^\[main.coverage.3\] file main.c line 10 function main MC/DC independence condition `!C && !D && A && !B.*: SATISFIED$
-^\[main.coverage.4\] file main.c line 10 function main MC/DC independence condition `!A && B && C && !D.*: SATISFIED$
-^\[main.coverage.5\] file main.c line 10 function main MC/DC independence condition `!A && !B && C && !D.*: SATISFIED$
+^\[main.coverage.\d+\] file main.c line 10 function main MC/DC independence condition `A && !B && C && !D.*: SATISFIED$
+^\[main.coverage.\d+\] file main.c line 10 function main MC/DC independence condition `!C && D && A && !B.*: SATISFIED$
+^\[main.coverage.\d+\] file main.c line 10 function main MC/DC independence condition `!C && !D && A && !B.*: SATISFIED$
+^\[main.coverage.\d+\] file main.c line 10 function main MC/DC independence condition `!A && B && C && !D.*: SATISFIED$
+^\[main.coverage.\d+\] file main.c line 10 function main MC/DC independence condition `!A && !B && C && !D.*: SATISFIED$
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring

src/goto-instrument/cover_util.cpp

@@ -48,36 +48,11 @@ std::set<exprt> collect_conditions(const exprt &src)
 
 std::set<exprt> collect_conditions(const goto_programt::const_targett t)
 {
-  switch(t->type)
-  {
-  case GOTO:
-  case ASSERT:
-    return collect_conditions(t->guard);
-
-  case ASSIGN:
-  case FUNCTION_CALL:
-    return collect_conditions(t->code);
-
-  case CATCH:
-  case THROW:
-  case DEAD:
-  case DECL:
-  case RETURN:
-  case ATOMIC_BEGIN:
-  case ATOMIC_END:
-  case START_THREAD:
-  case END_THREAD:
-  case END_FUNCTION:
-  case LOCATION:
-  case OTHER:
-  case SKIP:
-  case ASSUME:
-  case INCOMPLETE_GOTO:
-  case NO_INSTRUCTION_TYPE:
-    break;
-  }
+  std::set<exprt> result;
+
+  t->apply([&result](const exprt &e) { collect_conditions_rec(e, result); });
 
-  return std::set<exprt>();
+  return result;
 }
 
 void collect_operands(const exprt &src, std::vector<exprt> &dest)
@@ -120,43 +95,11 @@ void collect_decisions_rec(const exprt &src, std::set<exprt> &dest)
   }
 }
 
-std::set<exprt> collect_decisions(const exprt &src)
+std::set<exprt> collect_decisions(const goto_programt::const_targett t)
 {
   std::set<exprt> result;
-  collect_decisions_rec(src, result);
-  return result;
-}
 
-std::set<exprt> collect_decisions(const goto_programt::const_targett t)
-{
-  switch(t->type)
-  {
-  case GOTO:
-  case ASSERT:
-    return collect_decisions(t->guard);
-
-  case ASSIGN:
-  case FUNCTION_CALL:
-    return collect_decisions(t->code);
-
-  case CATCH:
-  case THROW:
-  case DEAD:
-  case DECL:
-  case RETURN:
-  case ATOMIC_BEGIN:
-  case ATOMIC_END:
-  case START_THREAD:
-  case END_THREAD:
-  case END_FUNCTION:
-  case LOCATION:
-  case OTHER:
-  case SKIP:
-  case ASSUME:
-  case INCOMPLETE_GOTO:
-  case NO_INSTRUCTION_TYPE:
-    break;
-  }
+  t->apply([&result](const exprt &e) { collect_decisions_rec(e, result); });
 
-  return std::set<exprt>();
+  return result;
 }