Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

crucible-syntax: Poor error message on program with uninitialized register #1025

Open
RyanGlScott opened this issue Aug 11, 2022 · 0 comments

Comments

@RyanGlScott
Copy link
Contributor

This program crashes with a rather confusing error message:

(defun @test () Unit
  (registers
    ($i Bool))

  (start start:
    (assert! (equal? $i $i) "Assertion")
    (return ())))
$ cabal run crucibler -- check test.cbl 
Up to date
crucibler: Input block type [BoolRepr] does not match expected []:
while SSA converting function test
CallStack (from HasCallStack):
  error, called at src/Lang/Crucible/CFG/SSAConversion.hs:976:24 in crucible-0.6-inplace:Lang.Crucible.CFG.SSAConversion

It seems like the semantics of registers are such that they have to be initialized before they can be used, as the error message goes away if an intervening (set-register! $i ...) statement is added. If so, the error message should say as much.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

1 participant