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

arm-hyp abstract: hypervisor fault not itself allowed to fault

This commit is contained in:
Gerwin Klein 2017-04-01 10:29:58 +02:00 committed by Alejandro Gomez-Londono
parent 115078328b
commit 04fae5af32
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
spec/abstract/ARM_HYP/Hypervisor_A.thy
View File

@ -16,10 +16,10 @@ begin
context Arch begin global_naming ARM_A
fun handle_hypervisor_fault :: "word32 \<Rightarrow> hyp_fault_type \<Rightarrow> (unit, 'z::state_ext) f_monad"
fun handle_hypervisor_fault :: "word32 \<Rightarrow> hyp_fault_type \<Rightarrow> (unit, 'z::state_ext) s_monad"
where
"handle_hypervisor_fault thread (ARMVCPUFault hsr) =
liftE (handle_fault thread (ArchFault $ VCPUFault hsr))"
handle_fault thread (ArchFault $ VCPUFault hsr)"
end