adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

arm crefine: Updates clearMemory_setObject_PTE_ccorres to use pteBits

This commit is contained in:
Alejandro Gomez-Londono 2017-06-05 15:06:06 +10:00
parent 4c1d294a75
commit 284cb43f7b
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
proof/crefine/ARM/Recycle_C.thy
View File

@ -645,7 +645,7 @@ lemma clearMemory_setObject_PTE_ccorres:
and (\<lambda>_. is_aligned ptr ptBits \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr))
(UNIV \<inter> {s. ptr___ptr_to_unsigned_long_' s = Ptr ptr} \<inter> {s. bits_' s = of_nat ptBits}) []
(do x \<leftarrow> mapM_x (\<lambda>a. setObject a ARM_H.InvalidPTE)
[ptr , ptr + 2 ^ objBits ARM_H.InvalidPTE .e. ptr + 2 ^ ptBits - 1];
[ptr , ptr + 2 ^ pteBits .e. ptr + 2 ^ ptBits - 1];
doMachineOp (cleanCacheRange_PoU ptr (ptr + 2 ^ ptBits - 1) pstart)
od)
(Call clearMemory_'proc)"