Print verification coverage only when -trace used (#770)

The -trackVerificationCoverage option enables tracking of verification
coverage but the results are printed only when -trace is also provided.
This makes it possible to see the results in text, but makes the output
less noisy for clients of Boogie as a library (such as Dafny).

Source/ExecutionEngine/ExecutionEngine.cs

@@ -673,7 +673,7 @@ private async Task<PipelineOutcome> VerifyEachImplementation(TextWriter output,
         CleanupRequest(requestId);
       }
 
-      if (Options.TrackVerificationCoverage && processedProgram.Program.AllCoveredElements.Any()) {
+      if (Options.Trace && Options.TrackVerificationCoverage && processedProgram.Program.AllCoveredElements.Any()) {
         Options.OutputWriter.WriteLine("Elements covered by verification: {0}", string.Join(", ", processedProgram.Program.AllCoveredElements.OrderBy(s => s)));
       }
 

Test/civl/samples/GC.bpl

@@ -293,6 +293,7 @@ requires call Yield_RootScanBarrierInv();
     call UpdateMutatorPhase(tid);
     call Yield_Iso();
     call ptr, absPtr := AllocRaw(tid, y);
+    assert {:layer 100} Iso(root, rootAbs, mem, memAbs, Color, toAbs, allocSet);
 }
 
 atomic action {:layer 101} AtomicWriteField({:linear "tid"} tid:Tid, x: idx, f: fld, y: idx) // x.f = y

Test/coverage/verificationCoverage.bpl

@@ -1,15 +1,28 @@
 // RUN: %boogie "%s" > "%t.plain"
-// RUN: %diff "%s.expect.plain" "%t.plain"
+// RUN: %diff "%s.expect" "%t.plain"
+// RUN: %boogie -trackVerificationCoverage -trace "%s" > "%t.coverage"
+// RUN  %OutputCheck "%s" --file-to-check="%t.coverage"
+// CHECK: Covered elements: a0, assert_a0, assert_r0, r0
+// CHECK: Covered elements: sinv_not_1$established, sinv_not_1$maintained, sinv1$assume_in_body, sinv1$established, sinv1$maintained, sinv2$assume_in_body, sinv2$established, sinv2$maintained, spost, spre1
+// CHECK: Covered elements: cont_assume_1, cont_assume_2
+// CHECK: Covered elements: false_req
+// CHECK: Covered elements: cont_req_1, cont_req_2
+// CHECK: Covered elements: assumeFalse
+// CHECK: Covered elements: tee0, tee1, ter0
+// CHECK: Covered elements: call2_tee1, tee_not_1, tee0$call1$ensures, tee0$call2$ensures, tee1$call2$ensures, ter0$call1$requires, ter0$call2$requires, ter1, xy_sum
+// CHECK: Covered elements: a_gt_10, constrained, x_gt_10
+// CHECK: Covered elements: cont_ens_abs$call_cont$ensures, xpos_abs$call_cont$requires, xpos_caller
+// CHECK: Elements covered by verification: a_gt_10, a0, assert_a0, assert_r0, assumeFalse, call2_tee1, constrained, cont_assume_1, cont_assume_2, cont_ens_abs$call_cont$ensures, cont_req_1, cont_req_2, false_req, r0, sinv_not_1$established, sinv_not_1$maintained, sinv1$assume_in_body, sinv1$established, sinv1$maintained, sinv2$assume_in_body, sinv2$established, sinv2$maintained, spost, spre1, tee_not_1, tee0, tee0$call1$ensures, tee0$call2$ensures, tee1, tee1$call2$ensures, ter0, ter0$call1$requires, ter0$call2$requires, ter1, x_gt_10, xpos_abs$call_cont$requires, xpos_caller, xy_sum
 // RUN: %boogie -trackVerificationCoverage "%s" > "%t.coverage"
-// RUN: %diff "%s.expect.coverage" "%t.coverage"
+// RUN: %diff "%s.expect" "%t.coverage"
 // RUN: %boogie -trackVerificationCoverage -typeEncoding:a -prune "%s" > "%t.coverage-a"
-// RUN: %diff "%s.expect.coverage" "%t.coverage-a"
+// RUN: %diff "%s.expect" "%t.coverage-a"
 // RUN: %boogie -trackVerificationCoverage -typeEncoding:p -prune "%s" > "%t.coverage-p"
-// RUN: %diff "%s.expect.coverage" "%t.coverage-p"
+// RUN: %diff "%s.expect" "%t.coverage-p"
 // RUN: %boogie -trackVerificationCoverage -normalizeDeclarationOrder:1 -prune "%s" > "%t.coverage-d"
-// RUN: %diff "%s.expect.coverage" "%t.coverage-d"
+// RUN: %diff "%s.expect" "%t.coverage-d"
 // RUN %boogie -trackVerificationCoverage -normalizeNames:1 -prune "%s" > "%t.coverage-n"
-// RUN %diff "%s.expect.coverage" "%t.coverage-n"
+// RUN %diff "%s.expect" "%t.coverage-n"
 // UNSUPPORTED: batch_mode
 
 procedure testRequiresAssign(n: int)

Test/unnecessaryassumes/unnecessaryassumes1.bpl

@@ -1,6 +1,9 @@
 // We use boogie instead of parallel-boogie here to fix the order of the output from /trackVerificationCoverage
-// RUN: %boogie /trackVerificationCoverage "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %boogie -trackVerificationCoverage -trace "%s" > "%t"
+// RUN: %OutputCheck "%s" --file-to-check="%t"
+// CHECK: Covered elements: s0
+// CHECK: Covered elements: s2, s3
+// CHECK: Elements covered by verification: s0, s2, s3
 // UNSUPPORTED: batch_mode
 
 procedure test0(n: int)