Skip to content

Extract and fix dead branch detection #353

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
Merged
merged 9 commits into from
Nov 26, 2021
Merged

Extract and fix dead branch detection #353

merged 9 commits into from
Nov 26, 2021

Conversation

@sim642
Copy link
Member

@sim642 sim642 commented Sep 21, 2021

This PR fixes some points in issue #346:

  1. Extract dead branch detection from base to Spec functor.

    This accounts for Deadcode raised by other analyses than base,
    but also cases where base's eval_rv is less precise than invariant.

  2. Fix locations for dead branches.

    Use if's location instead of first branch node's.
    This also makes always true conditions work when false branch is missing.

@sim642
Extract dead branch detection from base to Spec functor (issue #346)
0f83cac 
This accounts for Deadcode raised by other analyses than base,
but also cases where base's eval_rv is less precise than invariant.
@sim642
Comment base that invariant may be more precise than eval_rv
3274eeb
@sim642
Fix locations for dead branches (issue #346)
9b0e650 
Use if's location instead of first branch node's.
This also makes always true conditions work when false branch is missing.
@sim642
Remove TODOs from Juliet dead branch tests
cf9c875
@sim642
Enable dbg.print_dead_code in tests for Juliet
befc5e2
@sim642
Enable ana.int.interval in 50-juliet/08-CWE570_Expression_Always_Fals…
4ee59a9 
…e__02
@sim642 sim642 added cleanup Refactoring, clean-up bug labels Sep 21, 2021
michael-schwarz
michael-schwarz reviewed Nov 24, 2021
View reviewed changes
michael-schwarz
michael-schwarz reviewed Nov 24, 2021
View reviewed changes
michael-schwarz
michael-schwarz reviewed Nov 24, 2021
View reviewed changes
sim642
sim642 commented Nov 26, 2021
View reviewed changes
@michael-schwarz michael-schwarz merged commit 79fd8bd into master Nov 26, 2021
@michael-schwarz michael-schwarz deleted the dead-branch branch November 26, 2021 12:11
@sim642 sim642 mentioned this pull request Nov 26, 2021
Closed
6 tasks
@sim642 sim642 added this to the v2.0.0 milestone Aug 12, 2022
sim642 added a commit to sim642/opam-repository that referenced this pull request Aug 18, 2022
@sim642
[new release] goblint (2.0.0)
6efdfdf 
CHANGES:

Goblint "lean" release after a lot of cleanup.

* Remove unmaintained analyses: OSEK, ARINC, shapes, containment, deadlocksByRaces (goblint/analyzer#460, goblint/analyzer#736, goblint/analyzer#812, goblint/analyzer#474).
* Add interactive analysis (goblint/analyzer#391).
* Add server mode (goblint/analyzer#522).
* Add Compilation Database support (goblint/analyzer#406, goblint/analyzer#448).
* Add floating point domain, unrolled array domain and improved struct domains (goblint/analyzer#734, goblint/analyzer#761, goblint/analyzer#577, goblint/analyzer#419).
* Add static loop unrolling and heap variable unrolling (goblint/analyzer#563, goblint/analyzer#722).
* Improve race detection with may-happen-in-parallel analysis (goblint/analyzer#529, goblint/analyzer#518, goblint/analyzer#595).
* Reimplement lockset and deadlock analyses (goblint/analyzer#659, goblint/analyzer#662, goblint/analyzer#650, goblint/analyzer#655).
* Add pthread extraction to Promela (goblint/analyzer#220).
* Add location spans to output (goblint/analyzer#428, goblint/analyzer#449).
* Improve race reporting (goblint/analyzer#550, goblint/analyzer#551).
* Improve dead code reporting (goblint/analyzer#94, goblint/analyzer#353, goblint/analyzer#785).
* Refactor warnings (goblint/analyzer#55, goblint/analyzer#783).
* Add JSON schema for configuration (goblint/analyzer#476, goblint/analyzer#499).
* Refactor option names (goblint/analyzer#28, goblint/analyzer#192, goblint/analyzer#516, goblint/analyzer#675).
* Add bash completion (goblint/analyzer#669).
* Add OCaml 4.13 and 4.14 support, remove OCaml 4.09 support (goblint/analyzer#503, goblint/analyzer#672).
@sim642 sim642 mentioned this pull request Aug 18, 2022
Merged
sim642 added a commit to sim642/opam-repository that referenced this pull request Aug 18, 2022
@sim642
[new release] goblint (2.0.0)
1c281d5 
CHANGES:

Goblint "lean" release after a lot of cleanup.

* Remove unmaintained analyses: OSEK, ARINC, shapes, containment, deadlocksByRaces (goblint/analyzer#460, goblint/analyzer#736, goblint/analyzer#812, goblint/analyzer#474).
* Add interactive analysis (goblint/analyzer#391).
* Add server mode (goblint/analyzer#522).
* Add Compilation Database support (goblint/analyzer#406, goblint/analyzer#448).
* Add floating point domain, unrolled array domain and improved struct domains (goblint/analyzer#734, goblint/analyzer#761, goblint/analyzer#577, goblint/analyzer#419).
* Add static loop unrolling and heap variable unrolling (goblint/analyzer#563, goblint/analyzer#722).
* Improve race detection with may-happen-in-parallel analysis (goblint/analyzer#529, goblint/analyzer#518, goblint/analyzer#595).
* Reimplement lockset and deadlock analyses (goblint/analyzer#659, goblint/analyzer#662, goblint/analyzer#650, goblint/analyzer#655).
* Add pthread extraction to Promela (goblint/analyzer#220).
* Add location spans to output (goblint/analyzer#428, goblint/analyzer#449).
* Improve race reporting (goblint/analyzer#550, goblint/analyzer#551).
* Improve dead code reporting (goblint/analyzer#94, goblint/analyzer#353, goblint/analyzer#785).
* Refactor warnings (goblint/analyzer#55, goblint/analyzer#783).
* Add JSON schema for configuration (goblint/analyzer#476, goblint/analyzer#499).
* Refactor option names (goblint/analyzer#28, goblint/analyzer#192, goblint/analyzer#516, goblint/analyzer#675).
* Add bash completion (goblint/analyzer#669).
* Add OCaml 4.13 and 4.14 support, remove OCaml 4.09 support (goblint/analyzer#503, goblint/analyzer#672).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@michael-schwarz michael-schwarz michael-schwarz left review comments

Assignees

No one assigned

Labels

bug cleanup Refactoring, clean-up

Projects

None yet

Milestone

v2.0.0

Development

Successfully merging this pull request may close these issues.

3 participants

@sim642 @michael-schwarz