From 952c4068e84a64d38bd8d59409d664f2bb8c0853 Mon Sep 17 00:00:00 2001
From: Adrian Palacios <accorell@amazon.com>
Date: Mon, 8 Apr 2024 18:53:16 +0000
Subject: [PATCH] Better splits

---
 .../src/codegen_cprover_gotoc/codegen/function.rs  |  1 +
 .../src/codegen_cprover_gotoc/codegen/statement.rs |  2 +-
 kani-driver/src/coverage/cov_results.rs            | 14 +++++++++-----
 3 files changed, 11 insertions(+), 6 deletions(-)

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 }
     }
 }