Better splits

model-checking · Apr 9, 2024 · 0ae802b · 0ae802b
1 parent 2b9a771
commit 0ae802b
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 6 deletions.
diff --git 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
@@ -117,7 +117,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
@@ -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 }
     }
 }