From 438e27a8f1e3a0d22d508b5b58a6f465a32c2dcb Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@proofcraft.systems>
Date: Wed, 5 Jul 2023 17:46:00 +1000
Subject: [PATCH] aarch64 aspec: fix do_flush spec bug

cleanInvalidate should be using cleanInvalidateCacheRange_RAM.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
---
 spec/abstract/AARCH64/Arch_A.thy | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/spec/abstract/AARCH64/Arch_A.thy b/spec/abstract/AARCH64/Arch_A.thy
index 0ad8d3eb4..77c80678e 100644
--- a/spec/abstract/AARCH64/Arch_A.thy
+++ b/spec/abstract/AARCH64/Arch_A.thy
@@ -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;