rt arm refine: set handler params when configuring TCBs

Signed-off-by: Corey Lewis <[email protected]>
seL4 · Sep 2, 2022 · 7119752 · 7119752
1 parent e2e07dd
commit 7119752
Show file tree

Hide file tree

Showing 2 changed files with 161 additions and 97 deletions.
diff --git a/proof/refine/ARM/EmptyFail_H.thy b/proof/refine/ARM/EmptyFail_H.thy
@@ -287,7 +287,7 @@ lemma tcbEPFindIndex_empty_fail[intro!, wp, simp]:
   by (induct ci; subst tcbEPFindIndex.simps; simp)
 
 crunch (empty_fail) empty_fail: callKernel
-  (wp: empty_fail_catch)
+  (wp: empty_fail_catch simp: crunch_simps)
 
 theorem call_kernel_serial:
   "\<lbrakk> (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and