better tests

Author: danielsn

tests/expected/mmio/expected

@@ -0,0 +1,26 @@
+Status: SUCCESS\
+Description: "offset: attempt to compute number in bytes which would overflow"
+
+Status: SUCCESS\
+Description: "attempt to compute offset which would overflow"
+
+Status: FAILURE\
+Description: "dereference failure: pointer NULL"
+
+Status: SUCCESS
+Description: "dereference failure: pointer invalid"
+
+Status: FAILURE\
+Description: "dereference failure: deallocated dynamic object"
+
+Status: FAILURE\
+Description: "dereference failure: dead object"
+
+Status: FAILURE\
+Description: "dereference failure: pointer outside object bounds"
+
+Status: FAILURE\
+Description: "dereference failure: invalid integer address"
+
+Status: FAILURE\
+Description: "dereference failure: invalid integer address"

tests/expected/mmio/main.rs

@@ -0,0 +1,19 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+const BUFFER: *mut u32 = 0x8000 as *mut u32;
+const BUFFER2: *mut u32 = 0x1000 as *mut u32;
+
+#[cfg(kani)]
+#[kani::proof]
+#[kani::mmio_region(0x8000, 8)]
+fn test_write() {
+    let val = 12;
+    unsafe {
+        //BUFFER+2 is not in the MMIO region
+        *(BUFFER.offset(2)) = val;
+        //BUFFER2 is not in the MMIO region
+        *BUFFER2 = val;
+
+    }
+}

tests/kani/MMIO/test.rs

@@ -25,4 +25,16 @@ fn test_write2() {
         core::ptr::write_volatile(BUFFER2, val);
 
     }
+}
+
+#[cfg(kani)]
+#[kani::proof]
+#[kani::mmio_region(0x8000, 8)]
+/// Check that larger MMIO regions also work
+fn test_write3() {
+    let val = 12;
+    unsafe {
+        *BUFFER = val;
+        *(BUFFER.offset(1)) = val;
+    }
 }