Slight fudges for Fastpath use with PIDE.
This commit is contained in:
parent
4a56fb49f9
commit
f59767cdac
|
@ -56,6 +56,10 @@ session AInvs = ASpec +
|
||||||
* C Refinement proof.
|
* C Refinement proof.
|
||||||
*)
|
*)
|
||||||
|
|
||||||
|
session CRefineSyscall = CBaseRefine +
|
||||||
|
theories
|
||||||
|
"crefine/Syscall_C"
|
||||||
|
|
||||||
session CRefine = CBaseRefine +
|
session CRefine = CBaseRefine +
|
||||||
theories
|
theories
|
||||||
"crefine/Refine_C"
|
"crefine/Refine_C"
|
||||||
|
|
|
@ -2240,6 +2240,7 @@ lemma fastpath_call_ccorres:
|
||||||
split: Structures_H.kernel_object.splits)
|
split: Structures_H.kernel_object.splits)
|
||||||
done
|
done
|
||||||
show ?thesis
|
show ?thesis
|
||||||
|
using [[goals_limit = 1]]
|
||||||
apply (cinit lift: cptr_' msgInfo_')
|
apply (cinit lift: cptr_' msgInfo_')
|
||||||
apply (simp add: catch_liftE_bindE unlessE_throw_catch_If
|
apply (simp add: catch_liftE_bindE unlessE_throw_catch_If
|
||||||
unifyFailure_catch_If catch_liftE
|
unifyFailure_catch_If catch_liftE
|
||||||
|
@ -2872,7 +2873,6 @@ lemma threadSet_tcbState_valid_objs:
|
||||||
apply (clarsimp simp: valid_tcb'_def tcb_cte_cases_def)
|
apply (clarsimp simp: valid_tcb'_def tcb_cte_cases_def)
|
||||||
done
|
done
|
||||||
|
|
||||||
|
|
||||||
lemma fastpath_reply_wait_ccorres:
|
lemma fastpath_reply_wait_ccorres:
|
||||||
notes hoare_TrueI[simp]
|
notes hoare_TrueI[simp]
|
||||||
shows "ccorres dc xfdc
|
shows "ccorres dc xfdc
|
||||||
|
@ -2918,6 +2918,7 @@ lemma fastpath_reply_wait_ccorres:
|
||||||
done
|
done
|
||||||
|
|
||||||
show ?thesis
|
show ?thesis
|
||||||
|
using [[goals_limit = 1]]
|
||||||
apply (cinit lift: cptr_' msgInfo_')
|
apply (cinit lift: cptr_' msgInfo_')
|
||||||
apply (simp add: catch_liftE_bindE unlessE_throw_catch_If
|
apply (simp add: catch_liftE_bindE unlessE_throw_catch_If
|
||||||
unifyFailure_catch_If catch_liftE
|
unifyFailure_catch_If catch_liftE
|
||||||
|
|
Loading…
Reference in New Issue