Skip to content

Commit dc6044e

Browse files
committed
remove lemmas
1 parent 6621c44 commit dc6044e

1 file changed

Lines changed: 0 additions & 6 deletions

File tree

kernel/src/allocator.rs

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -612,12 +612,6 @@ impl<R: RegionDescriptor + Display + Copy> AppMemoryAllocator<R> {
612612
mpu::Permissions::ReadWriteOnly,
613613
);
614614
let memory_end = breaks.memory_start.wrapping_add(breaks.memory_size);
615-
ram_regions
616-
.fst
617-
.lemma_no_overlap_le_addr_implies_no_overlap_addr(breaks.app_break, memory_end);
618-
ram_regions
619-
.snd
620-
.lemma_no_overlap_le_addr_implies_no_overlap_addr(breaks.app_break, memory_end);
621615

622616
app_regions
623617
.get(FLASH_REGION_NUMBER)

0 commit comments

Comments
 (0)