From 09a49b7599157fd56f1ce2cb9c1877a8596690d7 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Wed, 21 Aug 2024 09:16:25 -0400 Subject: [PATCH] Heapster: Panic instead of calling partial head function (#2096) Really, we should be throwing a proper error message here instead of throwing a `panic`, and we should document the requirement that the list of mutually recursive functions must be non-empty. That is left as future work (see #2096). --- src/SAWScript/HeapsterBuiltins.hs | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/src/SAWScript/HeapsterBuiltins.hs b/src/SAWScript/HeapsterBuiltins.hs index d3511c5895..cb8af769ee 100644 --- a/src/SAWScript/HeapsterBuiltins.hs +++ b/src/SAWScript/HeapsterBuiltins.hs @@ -1076,7 +1076,15 @@ heapster_typecheck_mut_funs_rename :: BuiltinContext -> Options -> HeapsterEnv -> [(String, String, String)] -> TopLevel () heapster_typecheck_mut_funs_rename _bic opts henv fn_names_and_perms = - do let (fst_nm, _, _) = head fn_names_and_perms + do let (fst_nm, _, _) = + case fn_names_and_perms of + fn_name_and_perm:_ -> fn_name_and_perm + -- TODO: Give a proper error message here instead of panicking, + -- and document the non-empty list requirement. See #2096. + [] -> panic "heapster_typecheck_mut_funs_rename" + [ "Unexpected empty list of mutually recursive functions" + , "See https://github.com/GaloisInc/saw-script/issues/2096" + ] Some lm <- failOnNothing ("Could not find symbol definition: " ++ fst_nm) (lookupModDefiningSym henv fst_nm) let w = llvmModuleArchReprWidth lm