Skip to content

Commit 455523b

Browse files
committed
WIP: kani proofs
Signed-off-by: Babis Chalios <[email protected]>
1 parent 3928bf3 commit 455523b

File tree

1 file changed

+8
-0
lines changed
  • src/vmm/src/arch/aarch64

1 file changed

+8
-0
lines changed

src/vmm/src/arch/aarch64/mod.rs

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -232,6 +232,14 @@ mod verification {
232232

233233
let regions = arch_memory_regions(offset as usize, len as usize);
234234

235+
for region in &regions {
236+
println!(
237+
"region: [{:x}:{:x})",
238+
region.0.0,
239+
region.0.0 + region.1 as u64
240+
);
241+
}
242+
235243
// On Arm we have one MMIO gap that might fall within addressable ranges,
236244
// so we can get either 1 or 2 regions.
237245
assert!(regions.len() >= 1);

0 commit comments

Comments
 (0)