You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Consider the following program, written against Crucible's public API:
moduleMainwhereimportPreludeimportData.Parameterized.NonceimportData.Parameterized.SomeimportLang.Crucible.Backend.AssumptionStackmain::IO()
main =doSome gen <- newIONonceGenerator
stk <- initAssumptionStack gen
frameId <- pushFrame stk
_frameId <- pushFrame stk
_result <- popFrame @() frameId stk
putStrLn"No panic?"
This program panics:
%< ---------------------------------------------------
Revision: bb50c0d16922e13d6358ce9abc7042ed13feccab
Branch: master
Location: AssumptionStack.popFrame
Message: Push/pop mismatch in assumption stack!
*** Current frame: 0
*** Expected ident: 1
CallStack (from HasCallStack):
panic, called at src/Lang/Crucible/Panic.hs:11:9 in crucible-0.6-inplace:Lang.Crucible.Panic
panic, called at src/Lang/Crucible/Backend/AssumptionStack.hs:204:16 in crucible-0.6-inplace:Lang.Crucible.Backend.AssumptionStack
%< ---------------------------------------------------
I would argue that I have not found a bug in Crucible. More specifically, the only bug here is that this function calls panic when passed invalid arguments, but is exposed via a public API where such arguments may, in fact, be passed. This panic (and others like it) should either be reified in the return type (e.g., Either), or turned into a dedicated Exception instance (which should be noted in the Haddocks). Panics should be reserved for situations that are considered by Crucible to be literally impossible.
The text was updated successfully, but these errors were encountered:
Consider the following program, written against Crucible's public API:
This program panics:
I would argue that I have not found a bug in Crucible. More specifically, the only bug here is that this function calls
panic
when passed invalid arguments, but is exposed via a public API where such arguments may, in fact, be passed. This panic (and others like it) should either be reified in the return type (e.g.,Either
), or turned into a dedicatedException
instance (which should be noted in the Haddocks). Panics should be reserved for situations that are considered by Crucible to be literally impossible.The text was updated successfully, but these errors were encountered: