Prevent printing when --quiet is used (#2162)

Author: adpaco-aws

kani-driver/src/call_cbmc.rs

@@ -72,6 +72,7 @@ impl KaniSession {
                     kani_cbmc_output_filter(
                         i,
                         self.args.extra_pointer_checks,
+                        self.args.quiet,
                         &self.args.output_format,
                     )
                 })?;

kani-driver/src/cbmc_property_renderer.rs

@@ -168,6 +168,7 @@ impl ParserItem {
 pub fn kani_cbmc_output_filter(
     item: ParserItem,
     extra_ptr_checks: bool,
+    quiet: bool,
     output_format: &OutputFormat,
 ) -> Option<ParserItem> {
     // Some items (e.g., messages) are skipped.
@@ -178,9 +179,11 @@ pub fn kani_cbmc_output_filter(
     let processed_item = process_item(item, extra_ptr_checks);
     // Both formatting and printing could be handled by objects which
     // implement a trait `Printer`.
-    let formatted_item = format_item(&processed_item, output_format);
-    if let Some(fmt_item) = formatted_item {
-        println!("{fmt_item}");
+    if !quiet {
+        let formatted_item = format_item(&processed_item, output_format);
+        if let Some(fmt_item) = formatted_item {
+            println!("{fmt_item}");
+        }
     }
     // TODO: Record processed items and dump them into a JSON file
     // <https://github.com/model-checking/kani/issues/942>

tests/script-based-pre/check-quiet/assume.rs

@@ -0,0 +1,16 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#[kani::proof]
+fn assume1() {
+    let i: i32 = kani::any();
+    kani::assume(i < 10);
+    assert!(i < 20);
+}
+
+#[kani::proof]
+fn assume2() {
+    let i: u32 = kani::any();
+    kani::assume(i < 10);
+    assert!(i < 20);
+}

tests/script-based-pre/check-quiet/check-quiet.expected

@@ -0,0 +1 @@
+success: `--quiet` produced NO output

tests/script-based-pre/check-quiet/check-quiet.sh

@@ -0,0 +1,16 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# Checks that no output is produced if `--quiet` is used
+
+set -eu
+
+KANI_OUTPUT=`kani assume.rs --quiet | wc -l`
+
+if [[ ${KANI_OUTPUT} -ne 0 ]]; then
+    echo "error: \`--quiet\` produced some output"
+    exit 1
+else
+    echo "success: \`--quiet\` produced NO output"
+fi

tests/script-based-pre/check-quiet/config.yml

@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: check-quiet.sh
+expected: check-quiet.expected