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

arm-hyp abstract: correct loop range in vcpu_restore

This commit is contained in:
Miki Tanaka 2017-04-29 01:03:26 +10:00 committed by Alejandro Gomez-Londono
parent 79d7e5e4f8
commit c2d598b665
1 changed files with 2 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
spec/abstract/ARM_HYP/ArchVSpace_A.thy
View File

@ -486,11 +486,12 @@ where
vcpu \<leftarrow> get_vcpu vr; (* restore GIC VCPU control state *)
vgic \<leftarrow> return (vcpu_vgic vcpu);
num_list_regs \<leftarrow> gets (arm_gicvcpu_numlistregs \<circ> arch_state);
gicIndices \<leftarrow> return [0..<num_list_regs];
do_machine_op $ do
set_gic_vcpu_ctrl_vmcr (vgic_vmcr vgic);
set_gic_vcpu_ctrl_apr (vgic_apr vgic);
mapM (\<lambda>p. set_gic_vcpu_ctrl_lr (of_int (fst p)) (snd p))
(map (\<lambda>i. (i, (vgic_lr vgic) i)) [0 ..< num_list_regs + 1]);
(map (\<lambda>i. (i, (vgic_lr vgic) i)) gicIndices);
(* restore banked VCPU registers except SCTLR (that's in VCPUEnable) *)
set_lr_svc (vcpu_regs vcpu VCPURegLRsvc);
set_sp_svc (vcpu_regs vcpu VCPURegSPsvc);