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

x64: crefine: adjust register_from_H to use 32 word as per C code

This commit is contained in:
Joel Beeren 2017-09-21 16:03:24 +10:00
parent 38badfebfc
commit 87e169a78f
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
proof/crefine/X64/StateRelation_C.thy
View File

@ -219,7 +219,7 @@ definition
\<and> tcb_queue_relation getNext getPrev hp queue NULL qhead"
fun
register_from_H :: "register \<Rightarrow> machine_word"
register_from_H :: "register \<Rightarrow> 32 word"
where
"register_from_H X64.RAX = scast Kernel_C.RAX"
| "register_from_H X64.RBX = scast Kernel_C.RBX"