turns out only the comma seperated way works

Author: danielsn

kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs

@@ -405,16 +405,3 @@ fn extract_integer_argument(attr: &Attribute) -> Option<u128> {
         None
     }
 }
-
-// /// Extracts the integer value argument from the attribute provided
-// /// For example, `unwind(8)` return `Some(8)`
-// fn extract_integer_arguments(attr: &Attribute) -> Result<Vec<u128>, String> {
-//     // Vector of meta items , that contain the arguments given the attribute
-//     let attr_args = attr.meta_item_list().unwrap;
-//     Ok(attr_args.iter().map(|a| {
-//         match a.literal()?.kind {
-//             LitKind::Int(y, ..) => Some(y),
-//             _ => None,
-//         }
-//     }).collect())
-// }

kani-driver/src/call_cbmc.rs

@@ -96,10 +96,14 @@ impl KaniSession {
         }
 
         if !harness_metadata.mmio_regions.is_empty() {
-            for (start, len) in &harness_metadata.mmio_regions {
-                args.push("--mmio-regions".into());
-                args.push(format!("{}:{}", start, len).into());
-            }
+            args.push("--mmio-regions".into());
+            let mmio_string = harness_metadata
+                .mmio_regions
+                .iter()
+                .map(|(s, l)| format!("{}:{}", s, l))
+                .collect::<Vec<String>>()
+                .join(",");
+            args.push(mmio_string.into());
         }
 
         args.push("--slice-formula".into());

tests/kani/MMIO/test.rs

@@ -1,27 +1,28 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-#[cfg(kani)]
-const BUFFER: *mut u32 = 0xb8000 as *mut u32;
+const BUFFER: *mut u32 = 0x8000 as *mut u32;
+const BUFFER2: *mut u32 = 0x1000 as *mut u32;
 
+#[cfg(kani)]
 #[kani::proof]
-#[kani::mmio_region(0xb8000, 4)]
+#[kani::mmio_region(0x8000, 4)]
 fn test_write() {
     let val = 12;
     unsafe {
         core::ptr::write_volatile(BUFFER, val);
     }
 }
 
-// #[cfg(kani)]
-// #[kani::proof]
-// #[kani::mmio_region(0xb8000, 4)]
-// #[kani::mmio_region(0xbF000, 4)]
-// fn test_write2() {
-//     let val = 12;
-//     unsafe {
-//         core::ptr::write_volatile(BUFFER, val);
-//         core::ptr::write_volatile(BUFFER2, val);
+#[cfg(kani)]
+#[kani::proof]
+#[kani::mmio_region(0x8000, 4)]
+#[kani::mmio_region(0x1000, 4)]
+fn test_write2() {
+    let val = 12;
+    unsafe {
+        core::ptr::write_volatile(BUFFER, val);
+        core::ptr::write_volatile(BUFFER2, val);
 
-//     }
-// }
+    }
+}