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

Cryptic saw-verifier error when ghost state contains values of different types #543

Closed
langston-barrett opened this issue Sep 20, 2019 · 1 comment
Labels
subsystem: crucible-llvm Issues related to LLVM bitcode verification with crucible-llvm type: bug Issues reporting bugs or unexpected/unwanted behavior
Milestone

Comments

@langston-barrett
Copy link
Contributor

langston-barrett commented Sep 20, 2019

In the same vein as #542 when run on test_ghost_branch_03 from #541, saw-verifier yeilds this message when the ghost state has different types along different branches:

[22:17:09.062] Checking proof obligations h ...
== Anticipated failure message ==
user error ("crucible_llvm_verify" (/home/siddharthist/code/saw-script/intTests/test_ghost_branch_03/test.saw:36:10-36:30):
"z3" (/home/siddharthist/code/saw-script/intTests/test_ghost_branch_03/test.saw:36:71-36:73):
Verifier.SAW.Simulator.Prims.iteOp: malformed arguments: [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] <<boolean>>)
[22:17:09.065] done

Instead, we should disallow storing values of any type in ghost state, and make the declaration of a ghost variable explicitly typed.

@langston-barrett langston-barrett added type: bug Issues reporting bugs or unexpected/unwanted behavior subsystem: crucible-llvm Issues related to LLVM bitcode verification with crucible-llvm labels Sep 20, 2019
@atomb atomb added this to the 0.6 milestone May 5, 2020
@brianhuffman
Copy link
Contributor

Fixed by #550.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
subsystem: crucible-llvm Issues related to LLVM bitcode verification with crucible-llvm type: bug Issues reporting bugs or unexpected/unwanted behavior
Projects
None yet
Development

No branches or pull requests

3 participants