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.

Sign up for GitHub

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

Jump to bottom

"ambiguous collection of variables" #691

Closed
weaversa opened this issue Apr 27, 2020 · 3 comments
Closed

"ambiguous collection of variables" #691

weaversa opened this issue Apr 27, 2020 · 3 comments
Assignees
@brianhuffman
Labels
topics: error-messages Issues involving the messages SAW produces on error type: question Issues that are primarily asking questions usability An issue that impedes efficient understanding and use
Milestone
0.6

Comments

@weaversa
Copy link
Contributor

What does the error message mean?
@weaversa weaversa added the type: question Issues that are primarily asking questions label Apr 27, 2020
@atomb atomb added topics: error-messages Issues involving the messages SAW produces on error usability An issue that impedes efficient understanding and use labels Apr 28, 2020
@atomb atomb added this to the 0.6 milestone May 5, 2020
@weaversa
Copy link
Contributor Author

weaversa commented May 8, 2020

I think it means that crucible_fresh_var was called, but the fresh variables that were created were not tied to any input or output of the function being verified.

@atomb
Copy link
Contributor

atomb commented May 8, 2020

Yeah, that's basically right. Sorry for not answering this earlier! I've added it to the milestone for the next release to indicate that we should make this error message more useful before then.

@brianhuffman brianhuffman self-assigned this May 15, 2020
@brianhuffman
Copy link
Contributor

That same error condition can arise in two situations:

  • During verification, if a fresh variable declared in the post-state section is not reachable via points-to declarations from any function outputs (return value or globals)
  • When applying an override, if a fresh variable declared in the pre-state section is not reachable via points-to declarations from any function inputs (arguments or globals)

I'll write a new error message that should make sense in either context.

@brianhuffman brianhuffman mentioned this issue May 17, 2020
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@brianhuffman brianhuffman

Labels
topics: error-messages Issues involving the messages SAW produces on error type: question Issues that are primarily asking questions usability An issue that impedes efficient understanding and use
Projects
None yet
Milestone
0.6
Development

No branches or pull requests
3 participants
@atomb @brianhuffman @weaversa