diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index 195e90bd70c7..93ac1434a5e9 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -246,6 +246,7 @@ pub mod rustc_smir { // println!("COVERAGE: {:?}", &cov_info.mappings); for mapping in &cov_info.mappings { if mapping.kind.terms().next().unwrap() == coverage { + println!("COVERAGE: {:?}", mapping.code_region.clone()); return Some(mapping.code_region.clone()); } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 41c21603b49f..48a77c5f134b 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -107,7 +107,7 @@ impl<'tcx> GotocCtx<'tcx> { let instance = self.current_fn().instance_stable(); let cov_info = format!("{cov:?} ({fun})"); // NOTE: This helps see the coverage info we're processing - println!("COVERAGE: {:?} {:?} {:?}", cov, fun, stmt.span); + // println!("COVERAGE: {:?} {:?} {:?}", cov, fun, stmt.span); let cov_span = coverage_opaque_span(self.tcx, cov.clone(), instance); if let Some(code_region) = cov_span { let coverage_stmt = self.codegen_coverage(&cov_info, stmt.span, code_region); diff --git a/kani-driver/src/coverage/cov_results.rs b/kani-driver/src/coverage/cov_results.rs index 94eb00874d82..d42d642c460e 100644 --- a/kani-driver/src/coverage/cov_results.rs +++ b/kani-driver/src/coverage/cov_results.rs @@ -70,11 +70,15 @@ impl Display for CoverageRegion { impl CoverageRegion { pub fn from_str(str: String) -> Self { - let str_splits: Vec<&str> = str.split([':', '-']).map(|s| s.trim()).collect(); - assert_eq!(str_splits.len(), 5, "{str:?}"); - let file = str_splits[0].to_string(); - let start = (str_splits[1].parse().unwrap(), str_splits[2].parse().unwrap()); - let end = (str_splits[3].parse().unwrap(), str_splits[4].parse().unwrap()); + let blank_splits: Vec<&str> = str.split_whitespace().map(|s| s.trim()).collect(); + assert!(blank_splits[1] == "-"); + let str_splits1: Vec<&str> = blank_splits[0].split([':']).collect(); + let str_splits2: Vec<&str> = blank_splits[2].split([':']).collect(); + assert_eq!(str_splits1.len(), 3, "{str:?}"); + assert_eq!(str_splits2.len(), 2, "{str:?}"); + let file = str_splits1[0].to_string(); + let start = (str_splits1[1].parse().unwrap(), str_splits1[2].parse().unwrap()); + let end = (str_splits2[0].parse().unwrap(), str_splits2[1].parse().unwrap()); Self { file, start, end } } }