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

arm-hyp aspec: Fixing ird_idx initialization in vgic_maintenance

This commit is contained in:
Alejandro Gomez-Londono 2017-04-29 17:04:04 +10:00 committed by Alejandro Gomez-Londono
parent 1adc307094
commit 2d899a98a9
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/ArchInterrupt_A.thy
View File

@ -45,7 +45,7 @@ where
if eisr0 = 0 \<and> eisr1 = 0
then return $ VGICMaintenance None
else do
irq_idx \<leftarrow> return (if eisr0 \<noteq> 0 then word_ctz eisr0 else word_ctz eisr1);
irq_idx \<leftarrow> return (if eisr0 \<noteq> 0 then word_ctz eisr0 else word_ctz eisr1 + 32);
gic_vcpu_num_list_regs \<leftarrow> gets (arm_gicvcpu_numlistregs o arch_state);
when (irq_idx < gic_vcpu_num_list_regs) (do_machine_op $ do
virq \<leftarrow> get_gic_vcpu_ctrl_lr (of_nat irq_idx);