From 7b40ef3ad65bae6c2db7b6266b895129c0c89225 Mon Sep 17 00:00:00 2001
From: Adrian Palacios <accorell@amazon.com>
Date: Fri, 5 Apr 2024 18:47:34 +0000
Subject: [PATCH] Match on parentheses, all props need to match

---
 .../src/codegen_cprover_gotoc/codegen/statement.rs        | 2 +-
 kani-driver/src/call_cbmc.rs                              | 8 ++++++--
 kani-driver/src/coverage/coverage.rs                      | 3 ---
 library/kani/src/lib.rs                                   | 1 -
 4 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
index 939b6791c7e6..41c21603b49f 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -105,7 +105,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 
                 let fun = self.current_fn().readable_name();
                 let instance = self.current_fn().instance_stable();
-                let cov_info = format!("{cov:?} {fun}");
+                let cov_info = format!("{cov:?} ({fun})");
                 // NOTE: This helps see the coverage info we're processing
                 println!("COVERAGE: {:?} {:?} {:?}", cov, fun, stmt.span);
                 let cov_span = coverage_opaque_span(self.tcx, cov.clone(), instance);
diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs
index b5c9bd10835a..b2d170da4367 100644
--- a/kani-driver/src/call_cbmc.rs
+++ b/kani-driver/src/call_cbmc.rs
@@ -418,7 +418,7 @@ fn coverage_results_from_properties(properties: &[Property]) -> Option<CoverageR
         static RE: OnceLock<Regex> = OnceLock::new();
         RE.get_or_init(|| {
             Regex::new(
-                r#"^Coverage \{ kind: CounterIncrement\((?<counter_num>[0-9]+)\) \} (?<func_name>[_\d\w]+) - (?<span>.+)"#,
+                r#"^Coverage \{ kind: CounterIncrement\((?<counter_num>[0-9]+)\) \} \((?<func_name>[^)]+)\) - (?<span>.+)"#,
             )
             .unwrap()
         })
@@ -428,7 +428,7 @@ fn coverage_results_from_properties(properties: &[Property]) -> Option<CoverageR
         static RE: OnceLock<Regex> = OnceLock::new();
         RE.get_or_init(|| {
             Regex::new(
-                r#"^Coverage \{ kind: ExpressionUsed\((?<expr_num>[0-9]+)\) \} (?<func_name>[_\d\w]+) - (?<span>.+)"#,
+                r#"^Coverage \{ kind: ExpressionUsed\((?<expr_num>[0-9]+)\) \} \((?<func_name>[^)]+)\) - (?<span>.+)"#,
             )
             .unwrap()
         })
@@ -436,6 +436,8 @@ fn coverage_results_from_properties(properties: &[Property]) -> Option<CoverageR
     let mut coverage_results: BTreeMap<String, Vec<CoverageCheck>> = BTreeMap::default();
 
     for prop in cov_properties {
+        let mut prop_processed = false;
+
         if let Some(captures) = re.captures(&prop.description) {
             let function = demangle(&captures["func_name"]).to_string();
             let counter_num = &captures["counter_num"];
@@ -453,6 +455,7 @@ fn coverage_results_from_properties(properties: &[Property]) -> Option<CoverageR
             } else {
                 coverage_results.insert(file, vec![cov_check]);
             }
+            prop_processed = true;
         }
 
         if let Some(captures) = re2.captures(&prop.description) {
@@ -472,6 +475,7 @@ fn coverage_results_from_properties(properties: &[Property]) -> Option<CoverageR
             } else {
                 coverage_results.insert(file, vec![cov_check]);
             }
+            prop_processed = true;
         }
     }
 
diff --git a/kani-driver/src/coverage/coverage.rs b/kani-driver/src/coverage/coverage.rs
index ec3d2b8e65af..94922261dac4 100644
--- a/kani-driver/src/coverage/coverage.rs
+++ b/kani-driver/src/coverage/coverage.rs
@@ -13,9 +13,6 @@ use crate::harness_runner::HarnessResult;
 use anyhow::Result;
 use tracing::debug;
 
-
-use super::cov_results;
-
 pub fn coverage_cargo(mut session: KaniSession, _args: CargoCoverageArgs) -> Result<()> {
     session.args.coverage = true;
     let project = project::cargo_project(&session, false)?;
diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs
index c8ce3186d3c3..e3d27c4b1bfb 100644
--- a/library/kani/src/lib.rs
+++ b/library/kani/src/lib.rs
@@ -72,7 +72,6 @@ pub use futures::{block_on, block_on_with_spawn, spawn, yield_now, RoundRobin};
 #[cfg(not(feature = "concrete_playback"))]
 pub fn assume(cond: bool) {
     let _ = cond;
-    unreachable!("test");
 }
 
 #[inline(never)]