From f3bbd4753718ecb370602a5f25b0ee35ba38f017 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Fri, 19 May 2023 19:46:35 +1000 Subject: [PATCH] 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 --- spec/haskell/src/SEL4/Kernel/VSpace/AARCH64.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/haskell/src/SEL4/Kernel/VSpace/AARCH64.hs b/spec/haskell/src/SEL4/Kernel/VSpace/AARCH64.hs index 07b1aaf1e..76a2acace 100644 --- a/spec/haskell/src/SEL4/Kernel/VSpace/AARCH64.hs +++ b/spec/haskell/src/SEL4/Kernel/VSpace/AARCH64.hs @@ -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 })