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

x64: fix CR3 check in set_vm_root spec

This commit is contained in:
Matthew Brecknell 2017-02-15 18:50:59 +11:00
parent cdc4813228
commit 07b2241e37
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/X64/ArchVSpace_A.thy
View File

@ -208,7 +208,7 @@ definition
whenE (pml4 \<noteq> pml4') $ throwError InvalidRoot;
liftE $ update_asid_map asid;
curCR3 \<leftarrow> liftE $ getCurrentCR3;
whenE (CR3BaseAddress curCR3 \<noteq> pml4 \<or> CR3pcid curCR3 \<noteq> asid) $
whenE (curCR3 \<noteq> CR3 (addrFromPPtr pml4) asid) $
liftE $ setCurrentCR3 $ CR3 (addrFromPPtr pml4) asid
odE
| _ \<Rightarrow> throwError InvalidRoot) <catch>