arm crefine: fix decodeARMMMUInvocation branch hint

A previous update to C code added a disjunct to an `if` condition outside the existing `unlikely` branch hint. This commit is the proof update for a C patch that extends the branch hint to the full `if` condition. Signed-off-by: Matthew Brecknell <[email protected]>
seL4 · May 20, 2021 · 73649d2 · 73649d2
1 parent e9c7c48
commit 73649d2
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 2 deletions.
diff --git a/proof/crefine/ARM/Arch_C.thy b/proof/crefine/ARM/Arch_C.thy
@@ -3352,7 +3352,6 @@ lemma Arch_decodeInvocation_ccorres:
                   apply (rule_tac P = "rv'a = from_bool (\<not>( isUntypedCap (fst (hd extraCaps)) \<and>
                             capBlockSize (fst (hd extraCaps)) = objBits (makeObject ::asidpool)
                             ))" in ccorres_gen_asm2)
-                  apply csymbr
                 apply (rule ccorres_symb_exec_r)
                   apply (rule_tac xf'=ret__int_' in ccorres_abstract, ceqv)
                   apply (rule_tac P = "rv'b = from_bool (\<not>( isUntypedCap (fst (hd extraCaps)) \<and>

diff --git a/proof/crefine/ARM_HYP/Arch_C.thy b/proof/crefine/ARM_HYP/Arch_C.thy
@@ -3755,7 +3755,6 @@ lemma decodeARMMMUInvocation_ccorres:
                   apply (rule_tac P = "rv'a = from_bool (\<not>( isUntypedCap (fst (hd extraCaps)) \<and>
                             capBlockSize (fst (hd extraCaps)) = objBits (makeObject ::asidpool)
                             ))" in ccorres_gen_asm2)
-                  apply csymbr
                 apply (rule ccorres_symb_exec_r)
                   apply (rule_tac xf'=ret__int_' in ccorres_abstract, ceqv)
                   apply (rule_tac P = "rv'b = from_bool (\<not>( isUntypedCap (fst (hd extraCaps)) \<and>