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 = OnceLock::new(); RE.get_or_init(|| { Regex::new( - r#"^Coverage \{ kind: CounterIncrement\((?[0-9]+)\) \} (?[_\d\w]+) - (?.+)"#, + r#"^Coverage \{ kind: CounterIncrement\((?[0-9]+)\) \} \((?[^)]+)\) - (?.+)"#, ) .unwrap() }) @@ -428,7 +428,7 @@ fn coverage_results_from_properties(properties: &[Property]) -> Option = OnceLock::new(); RE.get_or_init(|| { Regex::new( - r#"^Coverage \{ kind: ExpressionUsed\((?[0-9]+)\) \} (?[_\d\w]+) - (?.+)"#, + r#"^Coverage \{ kind: ExpressionUsed\((?[0-9]+)\) \} \((?[^)]+)\) - (?.+)"#, ) .unwrap() }) @@ -436,6 +436,8 @@ fn coverage_results_from_properties(properties: &[Property]) -> Option> = 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 Option 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)]