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

InfoFlowC: updates for Hypervisor stub

This commit is contained in:
Miki Tanaka 2017-02-22 10:52:08 +11:00
parent fec4f5172a
commit a95b9cca7c
1 changed files with 12 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
proof/infoflow/ADT_IF_Refine_C.thy
View File

@ -107,7 +107,8 @@ definition
| UnknownSyscall n \<Rightarrow> (handleUnknownSyscall_C_body_if (of_nat n))
| UserLevelFault w1 w2 \<Rightarrow> (handleUserLevelFault_C_body_if w1 w2)
| Interrupt \<Rightarrow> (handleInterruptEntry_C_body_if)
| VMFaultEvent t \<Rightarrow> (handleVMFaultEvent_C_body_if (vm_fault_type_from_H t))"
| VMFaultEvent t \<Rightarrow> (handleVMFaultEvent_C_body_if (vm_fault_type_from_H t))
| HypervisorEvent t \<Rightarrow> (SKIP ;; \<acute>ret__unsigned_long :== scast EXCEPTION_NONE)"
definition
@ -294,6 +295,16 @@ lemma handleEvent_ccorres:
is_cap_fault_def
elim: pred_tcb'_weakenE st_tcb_ex_cap''
dest: st_tcb_at_idle_thread' rf_sr_ksCurThread)
-- "HypervisorEvent"
apply (simp add: liftE_def bind_assoc)
apply (rule ccorres_guard_imp2)
apply (rule ccorres_symb_exec_l)
apply (case_tac x6; simp add: handleHypervisorFault_def)
apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg)
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: return_def)
apply wp+
apply clarsimp
done
lemma kernelEntry_corres_C: