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

arm-hyp haskell: correct range_check fix for decodeVCPUInjectIRQ

This commit is contained in:
Miki Tanaka 2017-04-27 23:45:53 +10:00 committed by Alejandro Gomez-Londono
parent 2ed26c2c00
commit 8ca5198a7e
1 changed files with 4 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
spec/haskell/src/SEL4/Object/VCPU/ARM_HYP.lhs
View File

@ -232,7 +232,10 @@ FIXME ARMHYP: this does not at this instance correspond to exactly what the C
> rangeCheck grp (0::Int) 1
> gic_vcpu_num_list_regs <- withoutFailure $
> gets (armKSGICVCPUNumListRegs . ksArchState)
> rangeCheck index 0 (gic_vcpu_num_list_regs - 1)
>
> when (index >= fromIntegral gic_vcpu_num_list_regs) $
> (throw $ RangeError 0 (fromIntegral gic_vcpu_num_list_regs - 1))
>
> vcpuLR <- withoutFailure $ liftM (vgicLR . vcpuVGIC) $ getObject vcpuPtr
>
> when (vcpuLR ! (fromIntegral index) .&. vgicIRQMask == vgicIRQActive) $