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

aarch64 aspec: fix do_flush spec bug 

cleanInvalidate should be using cleanInvalidateCacheRange_RAM.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2023-07-05 17:46:00 +10:00
parent 7713dffccc
commit 438e27a8f1
No known key found for this signature in database
GPG Key ID: 20A847CE6AB7F5F3
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
spec/abstract/AARCH64/Arch_A.thy
View File

@ -116,7 +116,7 @@ definition do_flush :: "flush_type \<Rightarrow> vspace_ref \<Rightarrow> vspace
case type of
Clean \<Rightarrow> cleanCacheRange_RAM vstart vend pstart
| Invalidate \<Rightarrow> invalidateCacheRange_RAM vstart vend pstart
| CleanInvalidate \<Rightarrow> invalidateCacheRange_RAM vstart vend pstart
| CleanInvalidate \<Rightarrow> cleanInvalidateCacheRange_RAM vstart vend pstart
| Unify \<Rightarrow> do
cleanCacheRange_PoU vstart vend pstart;
dsb;