Do not directly handle an atomic condition within "collect_mcdc_controlling_rec".

Author: theyoucheng

regression/cbmc-cover/mcdc6/test.desc

@@ -3,8 +3,8 @@ main.c
 --cover mcdc
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.coverage.1\] file main.c line 4 function main MC/DC independence condition `!(x < (unsigned int)3).*: SATISFIED$
-^\[main.coverage.2\] file main.c line 4 function main MC/DC independence condition `x < (unsigned int)3.*: SATISFIED$
+^\[main.coverage.1\] file main.c line 4 function main decision/condition `x < (unsigned int)3.* false: SATISFIED$
+^\[main.coverage.2\] file main.c line 4 function main decision/condition `x < (unsigned int)3.* true: SATISFIED$
 ^\*\* .* of .* covered (100.0%)$
 ^\*\* Used 2 iterations$
 --

src/goto-instrument/cover.cpp

@@ -314,23 +314,28 @@ void collect_mcdc_controlling_rec(
   else if(src.id()==ID_not)
   {
     exprt e=to_not_expr(src).op();
-    collect_mcdc_controlling_rec(e, conditions, result);
-  }
-  else if(is_condition(src)) 
-  {
-    exprt e=src;
-    std::vector<exprt> new_conditions1=conditions;
-    new_conditions1.push_back(e);
-    result.insert(conjunction(new_conditions1));
-
-    //e.make_not();
-    std::vector<exprt> new_conditions2=conditions;
-    new_conditions2.push_back(not_exprt(e));
-    result.insert(conjunction(new_conditions2));
+    if(not is_condition(e))
+      collect_mcdc_controlling_rec(e, conditions, result);
+    else
+    {
+      // to store a copy of ''src''
+      std::vector<exprt> new_conditions1=conditions;
+      new_conditions1.push_back(src);
+      result.insert(conjunction(new_conditions1));
+
+      // to store a copy of its negation, i.e., ''e''
+      std::vector<exprt> new_conditions2=conditions;
+      new_conditions2.push_back(e);
+      result.insert(conjunction(new_conditions2));
+    }
   }
   else
   {
-    throw "Unexpected exprt for MC/DC coverage";
+    /**
+     * It may happen that ''is_condition(src)'' is valid,
+     * but we ignore this case here as it can be handled
+     * by the routine decision/condition detection.
+     **/
   }
 }