From baa55dfb362758406e4d7479e3a8712dbc5b1250 Mon Sep 17 00:00:00 2001 From: Sam Breese Date: Wed, 1 Jun 2022 16:01:57 -0400 Subject: [PATCH] Throw an exception when no candidates for an uninterpreted name are found (#1673) * Throw an exception when no uninterpreted names are found * Add an integration test --- intTests/test_resolve_unint_missing/test.saw | 1 + intTests/test_resolve_unint_missing/test.sh | 4 ++++ src/SAWScript/Builtins.hs | 8 +++++--- 3 files changed, 10 insertions(+), 3 deletions(-) create mode 100644 intTests/test_resolve_unint_missing/test.saw create mode 100644 intTests/test_resolve_unint_missing/test.sh diff --git a/intTests/test_resolve_unint_missing/test.saw b/intTests/test_resolve_unint_missing/test.saw new file mode 100644 index 0000000000..da680c1e8d --- /dev/null +++ b/intTests/test_resolve_unint_missing/test.saw @@ -0,0 +1 @@ +fails (prove_print (w4_unint_yices ["foo"]) {{ True }}); \ No newline at end of file diff --git a/intTests/test_resolve_unint_missing/test.sh b/intTests/test_resolve_unint_missing/test.sh new file mode 100644 index 0000000000..ae9efc9c46 --- /dev/null +++ b/intTests/test_resolve_unint_missing/test.sh @@ -0,0 +1,4 @@ +#!/bin/sh +set -e + +$SAW test.saw diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index d6404c0f35..a289a20e1c 100644 --- a/src/SAWScript/Builtins.hs +++ b/src/SAWScript/Builtins.hs @@ -515,12 +515,14 @@ resolveName sc nm = do resolvedName <- io $ scResolveNameByURI sc uri case resolvedName of Just vi -> pure $ vi:scnms - Nothing -> pure scnms - _ -> pure scnms - Nothing -> pure scnms + Nothing -> fallback scnms + _ -> fallback scnms + Nothing -> fallback scnms where tnm = Text.pack nm + fallback [] = fail $ "Could not resolve name: " <> show nm + fallback scnms = pure scnms normalize_term :: TypedTerm -> TopLevel TypedTerm