WIP: kani proofs

bchalios · bchalios · commit d1fda34590b4 · 2025-05-20T16:49:57.000+02:00
Signed-off-by: Babis Chalios &lt;bchalios@amazon.es&gt;
diff --git a/src/vmm/src/arch/x86_64/mod.rs b/src/vmm/src/arch/x86_64/mod.rs
@@ -522,6 +522,7 @@ mod verification {
                 assert_eq!(regions[1].0.0, FIRST_ADDR_PAST_32BITS);
             } else {
                 assert_eq!(regions[0].0.0 + regions[0].1 as u64, MMIO64_MEM_START);
+                assert_eq!(regions[1].0.0, FIRST_ADDR_PAST_64BITS_MMIO);
             }
         }
 

Original file line number	Diff line number	Diff line change
`@@ -522,6 +522,7 @@ mod verification {`
`522`	`522`	`assert_eq!(regions[1].0.0, FIRST_ADDR_PAST_32BITS);`
`523`	`523`	`} else {`
`524`	`524`	`assert_eq!(regions[0].0.0 + regions[0].1 as u64, MMIO64_MEM_START);`
	`525`	`+ assert_eq!(regions[1].0.0, FIRST_ADDR_PAST_64BITS_MMIO);`
`525`	`526`	`}`
`526`	`527`	`}`
`527`	`528`