Improve error messages for failed uninterpreted functions.

GaloisInc · Oct 20, 2020 · 7049e5c · 7049e5c
1 parent a489c57
commit 7049e5c
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 2 deletions.
diff --git 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
@@ -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
 
 
 ------------------------------------------------------------