From 7049e5c29975a36fc34b49fc410613f217f9c2df Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Tue, 20 Oct 2020 09:12:20 -0700 Subject: [PATCH] Improve error messages for failed uninterpreted functions. --- saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs | 3 ++- saw-core-what4/src/Verifier/SAW/Simulator/What4.hs | 3 ++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs b/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs index 5ff01115..c51dc3ce 100644 --- a/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs +++ b/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs @@ -268,7 +268,8 @@ flattenSValue v = do VNat n -> return ([], "_" ++ show n) TValue (suffixTValue -> Just s) -> return ([], s) - _ -> fail $ "Could not create sbv argument for " ++ show v + VFun _ -> fail "Cannot create uninterpreted higher-order function" + _ -> fail $ "Cannot create uninterpreted function with argument " ++ show v vWord :: SWord -> SValue vWord lv = VWord lv diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs index b9a0dbdf..f2c3d63c 100644 --- a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs +++ b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs @@ -828,7 +828,8 @@ applyUnintApp app0 v = VNat n -> return (suffixUnintApp ("_" ++ show n) app0) TValue (suffixTValue -> Just s) -> return (suffixUnintApp s app0) - _ -> fail $ "Could not create argument for " ++ show v + VFun _ -> fail "Cannot create uninterpreted higher-order function" + _ -> fail $ "Cannot create uninterpreted function with argument " ++ show v ------------------------------------------------------------