From e010665741f2a89a6e1169decc99f7f41cb24162 Mon Sep 17 00:00:00 2001
From: Adrian Palacios <accorell@amazon.com>
Date: Mon, 22 Apr 2024 21:06:03 +0000
Subject: [PATCH] Use square brackets to match on func. name
---
kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs | 2 +-
kani-driver/src/call_cbmc.rs | 4 ++--
2 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
index cc3cbbcefb85..18ab3341d54e 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -115,7 +115,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 9ac561e0cc60..956b646848dc 100644
--- a/kani-driver/src/call_cbmc.rs
+++ b/kani-driver/src/call_cbmc.rs
@@ -419,7 +419,7 @@ fn coverage_results_from_properties(properties: &[Property]) -> Option<CoverageR
static RE: OnceLock<Regex> = OnceLock::new();
RE.get_or_init(|| {
Regex::new(
- r#"^CounterIncrement\((?<counter_num>[0-9]+)\) \((?<func_name>[^)]+)\) - (?<span>.+)"#,
+ r#"^CounterIncrement\((?<counter_num>[0-9]+)\) \[(?<func_name>[^\]]+)\] - (?<span>.+)"#,
)
.unwrap()
})
@@ -429,7 +429,7 @@ fn coverage_results_from_properties(properties: &[Property]) -> Option<CoverageR
static RE: OnceLock<Regex> = OnceLock::new();
RE.get_or_init(|| {
Regex::new(
- r#"^ExpressionUsed\((?<expr_num>[0-9]+)\) \((?<func_name>[^)]+)\) - (?<span>.+)"#,
+ r#"^ExpressionUsed\((?<expr_num>[0-9]+)\) \[(?<func_name>[^\]]+)\] - (?<span>.+)"#,
)
.unwrap()
})