diff --git a/spec/abstract/RISCV64/Machine_A.thy b/spec/abstract/RISCV64/Machine_A.thy index bebed7805..e4324e749 100644 --- a/spec/abstract/RISCV64/Machine_A.thy +++ b/spec/abstract/RISCV64/Machine_A.thy @@ -109,7 +109,7 @@ definition msg_label_bits :: nat definition new_context :: "user_context" where - "new_context \ UserContext (\_. 0)" + "new_context \ UserContext ((\_. 0) (SSTATUS := sstatusSPIE))" text \ The lowest virtual address in the kernel window. The kernel reserves the virtual addresses