make bmc_cover work, and test it

Author: Daniel Kroening

regression/cbmc-cover/Makefile

@@ -0,0 +1,20 @@
+default: tests.log
+
+test:
+	@if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \
+		../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
+
+tests.log: ../test.pl
+	@if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \
+		../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;

regression/cbmc-cover/branch1/main.c

@@ -0,0 +1,17 @@
+int main()
+{
+  int input1, input2;
+  
+  if(input1)
+  {
+    if(input1) // dependent
+    {
+    }
+  }
+  else
+  {
+    if(input2) // independent
+    {
+    }
+  }
+}

regression/cbmc-cover/branch1/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--cover branch
+^EXIT=0$
+^SIGNAL=0$
+^\[main.1\] file main.c line 5 function main function main block 1 branch false: SATISFIED$
+^\[main.2\] file main.c line 5 function main function main block 1 branch true: SATISFIED$
+^\[main.3\] file main.c line 7 function main function main block 2 branch false: FAILED$
+^\[main.4\] file main.c line 7 function main function main block 2 branch true: SATISFIED$
+^\[main.5\] file main.c line 13 function main function main block 4 branch false: SATISFIED$
+^\[main.6\] file main.c line 13 function main function main block 4 branch true: SATISFIED$
+--
+^warning: ignoring

regression/cbmc-cover/condition1/main.c

@@ -0,0 +1,17 @@
+int main()
+{
+  int input1, input2;
+  
+  if(input1 && input2)
+  {
+  }
+  else if(input1)
+  {
+  }
+  else if(input2)
+  {
+    if(input1) // can't be true
+    {
+    }
+  }
+}

regression/cbmc-cover/condition1/test.desc

@@ -0,0 +1,18 @@
+CORE
+main.c
+--cover condition
+^EXIT=0$
+^SIGNAL=0$
+^\[main.1] file main.c line 5 function main condition .* false: SATISFIED
+^\[main.2] file main.c line 5 function main condition .* true: SATISFIED
+^\[main.3] file main.c line 5 function main condition .* false: SATISFIED
+^\[main.4] file main.c line 5 function main condition .* true: SATISFIED
+^\[main.5] file main.c line 8 function main condition .* false: SATISFIED
+^\[main.6] file main.c line 8 function main condition .* true: SATISFIED
+^\[main.7] file main.c line 11 function main condition .* false: SATISFIED
+^\[main.8] file main.c line 11 function main condition .* true: SATISFIED
+^\[main.9] file main.c line 13 function main condition .* false: FAILED
+^\[main.10] file main.c line 13 function main condition .* true: SATISFIED
+^\*\* 9 of 10 covered (90.0%)
+--
+^warning: ignoring

regression/cbmc-cover/decision1/main.c

@@ -0,0 +1,11 @@
+int main()
+{
+  int input1, input2, input3;
+  
+  if(input1 && input2 && input3)
+  {
+  }
+  else
+  {
+  }
+}

regression/cbmc-cover/decision1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--cover decision
+^EXIT=0$
+^SIGNAL=0$
+^\*\* 2 of 2 covered (100.0%), using 2 iterations$
+--
+^warning: ignoring

regression/cbmc-cover/location1/main.c

@@ -0,0 +1,15 @@
+int main()
+{
+  int input1;
+  int x=0;
+  
+  if(input1)
+  {
+    x=1;
+  }
+
+  if(input1 && !x)
+  {
+    x=2; // I am dead!
+  }
+}

regression/cbmc-cover/location1/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--cover location
+^EXIT=0$
+^SIGNAL=0$
+^\[main.1\] file main.c line 3 function main block 1: SATISFIED$
+^\[main.2\] file main.c line 8 function main block 2: SATISFIED$
+^\[main.3\] file main.c line 11 function main block 3: SATISFIED$
+^\[main.4\] file main.c line 13 function main block 4: FAILED$
+^\[main.5\] file main.c line 15 function main block 5: SATISFIED$
+^\*\* 4 of 5 covered (80.0%)
+--
+^warning: ignoring

src/cbmc/bmc_cover.cpp

@@ -272,33 +272,33 @@ bool bmc_covert::operator()()
             i_it->source_location);
     }
   }
+
+  for(symex_target_equationt::SSA_stepst::iterator
+      it=bmc.equation.SSA_steps.begin();
+      it!=bmc.equation.SSA_steps.end();
+      it++)
+    it->cond_literal=literalt(0, 0);
 
   // Do conversion to next solver layer
 
   bmc.do_conversion();
 
   //bmc.equation.output(std::cout);
 
-  // collects assumptions
-  and_exprt::operandst assumptions;
-
   // get the conditions for these goals from formula
   // collect all 'instances' of the goals
   for(symex_target_equationt::SSA_stepst::iterator
       it=bmc.equation.SSA_steps.begin();
       it!=bmc.equation.SSA_steps.end();
       it++)
   {
-    if(it->is_assume())
-      assumptions.push_back(literal_exprt(it->cond_literal));
-  
-    if(it->source.pc->is_assert())
+    if(it->is_assert())
     {
+      assert(it->source.pc->is_assert());
       exprt c=
         conjunction({
-          conjunction(assumptions), 
           literal_exprt(it->guard_literal),
-          literal_exprt(it->cond_literal) });
+          literal_exprt(!it->cond_literal) });
       literalt l_c=solver.convert(c);
       goal_map[id(it->source.pc)].add_instance(it, l_c);
     }

src/goto-instrument/cover.cpp

@@ -301,9 +301,7 @@ void instrument_cover_goals(
           if(!source_location.get_file().empty() &&
              source_location.get_file()[0]!='<')
           {
-            std::string comment=
-              "block "+i2string(i_it->location_number);
-
+            std::string comment="block "+b;
             goto_program.insert_before_swap(i_it);
             i_it->make_assertion(false_exprt());
             i_it->source_location=source_location;
@@ -328,12 +326,12 @@ void instrument_cover_goals(
         source_locationt source_location=i_it->source_location;
 
         goto_program.insert_before_swap(i_it);
-        i_it->make_assertion(guard);
+        i_it->make_assertion(not_exprt(guard));
         i_it->source_location=source_location;
         i_it->source_location.set_comment(true_comment);
 
         goto_program.insert_before_swap(i_it);
-        i_it->make_assertion(not_exprt(guard));
+        i_it->make_assertion(guard);
         i_it->source_location=source_location;
         i_it->source_location.set_comment(false_comment);