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

reduce UserLevelFault code to 28 bits 

This makes room for a 4-bit seL4_FaultType field.
This commit is contained in:
Matthew Brecknell 2019-06-18 12:04:43 +10:00
parent 4e12863b0f
commit 2e556d4a33
3 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
spec/abstract/Syscall_A.thy
View File

@ -349,7 +349,7 @@ where
| "handle_event (UserLevelFault w1 w2) = (without_preemption $ do
thread \<leftarrow> gets cur_thread;
handle_fault thread $ UserException (w1 && mask 32) (w2 && mask 29);
handle_fault thread $ UserException (w1 && mask 32) (w2 && mask 28);
return ()
od)"

2
spec/haskell/src/SEL4/API/Syscall.lhs
View File

@ -127,7 +127,7 @@ bottom 32 bits be communicated to the fault handler, for the second word
> handleEvent (UserLevelFault w1 w2) = withoutPreemption $ do
> thread <- getCurThread
> handleFault thread $ UserException (w1 .&. mask 32) (w2 .&. mask 29)
> handleFault thread $ UserException (w1 .&. mask 32) (w2 .&. mask 28)
> return ()
\subsubsection{Virtual Memory Faults}

2
spec/sep-abstract/Syscall_SA.thy
View File

@ -216,7 +216,7 @@ where
| "handle_event (UserLevelFault w1 w2) = (without_preemption $ do
thread \<leftarrow> gets cur_thread;
handle_fault thread $ UserException w1 (w2 && mask 29);
handle_fault thread $ UserException w1 (w2 && mask 28);
return ()
od)"