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

arm-hyp abstract: correct make_virq

This commit is contained in:
Miki Tanaka 2017-04-28 00:16:03 +10:00 committed by Alejandro Gomez-Londono
parent 100ac2cee1
commit c06b58f369
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/VCPU_A.thy
View File

@ -165,7 +165,7 @@ definition make_virq :: "obj_ref \<Rightarrow> obj_ref \<Rightarrow> obj_ref \<R
prioShift = 23;
irqPending = 1 << 28;
eoiirqen = 1 << 19
in (grp << groupShift) || (prio << prioShift) || irq || irqPending || eoiirqen"
in ((grp && 1) << groupShift) || ((prio && 0x1F) << prioShift) || (irq && 0x3FF) || irqPending || eoiirqen"
definition decode_vcpu_inject_irq :: "obj_ref list \<Rightarrow> arch_cap \<Rightarrow> (arch_invocation,'z::state_ext) se_monad"