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

arm-hyp abtract: change invoke_vcpu_inject_irq definition for better matchin

This commit is contained in:
Miki Tanaka 2017-04-27 10:05:05 +10:00 committed by Alejandro Gomez-Londono
parent 4e98e6e2a5
commit 7067365560
1 changed files with 4 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -194,13 +194,13 @@ where
definition invoke_vcpu_inject_irq :: "obj_ref \<Rightarrow> nat \<Rightarrow> virq \<Rightarrow> (unit,'z::state_ext) s_monad"
where "invoke_vcpu_inject_irq vr index virq \<equiv> do
cur_v \<leftarrow> gets (arm_current_vcpu \<circ> arch_state);
(case cur_v of
Some (vr, _) \<Rightarrow> do_machine_op $ set_gic_vcpu_ctrl_lr (of_nat index) virq
| None \<Rightarrow> do
if (cur_v \<noteq> None \<and> fst (the cur_v) = vr)
then do_machine_op $ set_gic_vcpu_ctrl_lr (of_nat index) virq
else do
vcpu \<leftarrow> get_vcpu vr;
vcpuLR \<leftarrow> return $ (vgic_lr $ vcpu_vgic vcpu) (index := virq);
set_vcpu vr $ vcpu \<lparr> vcpu_vgic := (vcpu_vgic vcpu) \<lparr> vgic_lr := vcpuLR \<rparr>\<rparr>
od)
od
od"
text {* VCPU perform and decode main functions *}