Match on parentheses, all props need to match

model-checking · Apr 5, 2024 · 7b40ef3 · 7b40ef3
1 parent e17f8b9
commit 7b40ef3
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 7 deletions.
diff --git 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
@@ -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,14 +428,16 @@ 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()
         })
     };
     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
@@ -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
@@ -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)]