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

arm-hyp abstract: fix order of VCPUSet arguments

This commit is contained in:
Gerwin Klein 2017-03-21 21:19:50 +11:00 committed by Alejandro Gomez-Londono
parent 4260a2c545
commit db3ffbd4b6
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
spec/abstract/ARM_HYP/VCPU_A.thy
View File

@ -209,7 +209,7 @@ text {* VCPU perform and decode main functions *}
definition
perform_vcpu_invocation :: "vcpu_invocation \<Rightarrow> (data list,'z::state_ext) s_monad" where
"perform_vcpu_invocation iv \<equiv> case iv of
VCPUSetTCB vcpu tcb \<Rightarrow> do associate_vcpu_tcb tcb vcpu; return [] od
VCPUSetTCB vcpu tcb \<Rightarrow> do associate_vcpu_tcb vcpu tcb; return [] od
| VCPUReadRegister vcpu reg \<Rightarrow> invoke_vcpu_read_register vcpu reg
| VCPUWriteRegister vcpu reg val \<Rightarrow> do invoke_vcpu_write_register vcpu reg val; return [] od
| VCPUInjectIRQ vcpu index vir \<Rightarrow> do invoke_vcpu_inject_irq vcpu index vir; return [] od"