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

aarch64 haskell: prefer fail over error 

`error` is mapped to `undefined` which does not work well with `crunch`.
`fail` is mapped to monadic `fail` in Isabelle, works fine with crunch
and we have to prove that it's not called in `corres`.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2023-05-19 19:46:35 +10:00
parent 4834c2589a
commit f3bbd47537
No known key found for this signature in database
GPG Key ID: 20A847CE6AB7F5F3
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/haskell/src/SEL4/Kernel/VSpace/AARCH64.hs
View File

@ -407,7 +407,7 @@ loadVMID asid = do
maybeEntry <- getASIDPoolEntry asid
case maybeEntry of
Just (ASIDPoolVSpace vmID ptr) -> return vmID
_ -> error ("loadVMID: no entry for asid")
_ -> fail "loadVMID: no entry for asid"
invalidateASID :: ASID -> Kernel ()
invalidateASID = updateASIDPoolEntry (\entry -> Just $ entry { apVMID = Nothing })