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

x64: crefine: fix default case in vmrights_to_H

This commit is contained in:
Joel Beeren 2017-10-03 10:56:43 +11:00
parent f24785cb8b
commit 1069cb70f2
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
proof/crefine/X64/Wellformed_C.thy
View File

@ -197,9 +197,9 @@ definition
definition
vmrights_to_H :: "word64 \<Rightarrow> vmrights" where
"vmrights_to_H c \<equiv>
if c = scast Kernel_C.VMKernelOnly then VMKernelOnly
if c = scast Kernel_C.VMReadWrite then VMReadWrite
else if c = scast Kernel_C.VMReadOnly then VMReadOnly
else VMReadWrite"
else VMKernelOnly"
(* Force clarity over name collisions *)
abbreviation