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

Spurious unwindset-does-not-match-any-loop warnings #88

Closed
tautschnig opened this issue Feb 2, 2022 · 1 comment
Closed

Spurious unwindset-does-not-match-any-loop warnings #88

tautschnig opened this issue Feb 2, 2022 · 1 comment
Assignees
@tautschnig
Labels
bug Something isn't working

Comments

@tautschnig
Copy link
Member

We had two changes the combination of which may result in spurious warnings:

  • As of dbf54250243dfa4c we perform (some) loop unwinding using goto-instrument.
  • With CBMC versions >= 5.46.0, there are warnings issued for loop identifiers that occur in --unwindset, but don't actually exist in the program. With goto-instrument's loop unwinding, loops are removed, and cbmc will therefore complain about non-existent loops.

Users will now see a mix of genuine and spurious warnings about non-existent loops. To avoid warning fatigue, we should figure out a way to avoid spurious (while still keeping the genuine ones!) warnings.
@tautschnig tautschnig added the bug Something isn't working label Feb 2, 2022
@tautschnig tautschnig self-assigned this Feb 2, 2022
@muneebahmed10 muneebahmed10 mentioned this issue Feb 2, 2022
Merged
@markrtuttle markrtuttle mentioned this issue May 9, 2022
Merged
@markrtuttle
Copy link
Contributor

Resolved by #110

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@tautschnig tautschnig

Labels
bug Something isn't working
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@tautschnig @markrtuttle