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

arm-hyp abstract: add missing isb machine op in vcpu_disable

This commit is contained in:
Miki Tanaka 2017-04-21 20:58:17 +10:00 committed by Alejandro Gomez-Londono
parent 16b6f26483
commit 69adb29a89
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

@ -333,7 +333,8 @@ where
hcr \<leftarrow> do_machine_op get_gic_vcpu_ctrl_hcr;
sctlr \<leftarrow> do_machine_op getSCTLR;
regs' \<leftarrow> return $ (vcpu_regs vcpu) (VCPURegSCTLR := sctlr);
set_vcpu vr (vcpu\<lparr> vcpu_vgic := (vcpu_vgic vcpu)\<lparr> vgic_hcr := hcr \<rparr>, vcpu_regs := regs'\<rparr>)
set_vcpu vr (vcpu\<lparr> vcpu_vgic := (vcpu_vgic vcpu)\<lparr> vgic_hcr := hcr \<rparr>, vcpu_regs := regs'\<rparr>);
do_machine_op isb
od
| _ \<Rightarrow> return ());
do_machine_op $ do