Skip to content

Conversation

@michael-schwarz
Copy link
Member

@michael-schwarz michael-schwarz commented Oct 7, 2022

This adds a warning when both branches of a condition are unreachable, usually hinting at an issue in the analyzer. Does not produce such warnings for edges with guard 1, as Goblint adds Neg(1) edges to ensure connectedness of CFGs.

Closes #826.

@michael-schwarz michael-schwarz added unsound debugging Abstract debugging labels Oct 7, 2022
@michael-schwarz michael-schwarz requested a review from sim642 October 7, 2022 15:54
Copy link
Member

@sim642 sim642 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Catches the problem from #750 👍

@sim642 sim642 merged commit 0baab72 into master Oct 10, 2022
@sim642 sim642 deleted the issue_826 branch October 10, 2022 07:26
@michael-schwarz michael-schwarz added the hacktoberfest-accepted https://hacktoberfest.digitalocean.com/ label Oct 24, 2022
@sim642 sim642 added this to the v2.1.0 milestone Nov 21, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

debugging Abstract debugging hacktoberfest-accepted https://hacktoberfest.digitalocean.com/ unsound

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Sanity check both branches not dead

3 participants