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

riscv aspec: initialise SSTATUS register correctly

This commit is contained in:
Gerwin Klein 2019-07-17 19:40:36 +10:00
parent 46398221c9
commit c77b2126e0
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/RISCV64/Machine_A.thy
View File

@ -109,7 +109,7 @@ definition msg_label_bits :: nat
definition new_context :: "user_context"
where
"new_context \<equiv> UserContext (\<lambda>_. 0)"
"new_context \<equiv> UserContext ((\<lambda>_. 0) (SSTATUS := sstatusSPIE))"
text \<open>
The lowest virtual address in the kernel window. The kernel reserves the virtual addresses