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

arm-hyp haskell: change invokeVCPUInjectIRQ definition for better matching

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

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

@ -246,13 +246,13 @@ FIXME ARMHYP: this does not at this instance correspond to exactly what the C
> invokeVCPUInjectIRQ :: PPtr VCPU -> Int -> VIRQ -> Kernel [Word]
> invokeVCPUInjectIRQ vcpuPtr index virq = do
> hsCurVCPU <- gets (armHSCurVCPU . ksArchState)
> case hsCurVCPU of
> Just (vcpuPtr, _) ->
> doMachineOp $ set_gic_vcpu_ctrl_lr (fromIntegral index) virq
> _ -> do
> vcpu <- getObject vcpuPtr
> let vcpuLR = (vgicLR . vcpuVGIC $ vcpu) // [(index, virq)]
> setObject vcpuPtr $ vcpu { vcpuVGIC = (vcpuVGIC vcpu) { vgicLR = vcpuLR }}
> if (isJust hsCurVCPU && fst (fromJust hsCurVCPU) == vcpuPtr)
> then
> doMachineOp $ set_gic_vcpu_ctrl_lr (fromIntegral index) virq
> else do
> vcpu <- getObject vcpuPtr
> let vcpuLR = (vgicLR . vcpuVGIC $ vcpu) // [(index, virq)]
> setObject vcpuPtr $ vcpu { vcpuVGIC = (vcpuVGIC vcpu) { vgicLR = vcpuLR }}
> return []