Skip to content

Commit

Permalink
resolveSpecName: Panic instead of calling partial tail function (#2097)
Browse files Browse the repository at this point in the history
Really, we should be throwing a proper error message here instead of throwing a
`panic`, and we should document the requirement that `__breakpoint__` functions
must end with `#<parent_name>`. That is left as future work (see #2097).
  • Loading branch information
RyanGlScott committed Aug 21, 2024
1 parent 09a49b7 commit 738f1dc
Showing 1 changed file with 14 additions and 4 deletions.
18 changes: 14 additions & 4 deletions src/SAWScript/Crucible/LLVM/Builtins.hs
Original file line number Diff line number Diff line change
Expand Up @@ -281,10 +281,20 @@ findDecl llmod nm =
resolveSpecName :: String -> TopLevel (String, Maybe String)
resolveSpecName nm =
if Crucible.testBreakpointFunction nm
then return
( (takeWhile (not . (== '#')) nm)
, Just (tail (dropWhile (not . (== '#')) nm))
)
then
let parentName =
case dropWhile (not . (== '#')) nm of
_:parentName' -> parentName'
-- TODO: Give a proper error message here instead of panicking,
-- and document __breakpoint__ naming requirements. See #2097.
[] -> panic "resolveSpecName"
[ "__breakpoint__ function not followed by #<parent_name>"
, "See https://github.com/GaloisInc/saw-script/issues/2097"
] in
return
( (takeWhile (not . (== '#')) nm)
, Just parentName
)
else return (nm, Nothing)

llvm_verify ::
Expand Down

0 comments on commit 738f1dc

Please sign in to comment.