Filter non-racing accesses of racing variable #550
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
Umm... what?! Why did pushing a9e03d8 to Whatever, if there's a problem with this, we can still discuss it here and fix it directly on master. |
|
I was also surprised why you'd request a review and then merge it immediately 😉 The only question is whether we may want to explicitly mention somewhere in the output that we only print accesses potentially involved in a race? |
|
I think it's fine not to, especially since the old behavior was more confusing: the race warning listed accesses that didn't actually race with anything and there was no mention of that. Also, with |
sim642
added a commit
to sim642/opam-repository
that referenced
this pull request
Aug 18, 2022
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
added a commit
to sim642/opam-repository
that referenced
this pull request
Aug 18, 2022
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
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Previously, if we determined a variable to have racing accesses, then we printed all of its accesses. This is excessive since there might be accesses that don't race with any other.
This PR filters the accesses of a racing variable to only contain those that actually race with another access to it. This is now possible due to the pairwise may-race checking and avoids some spurious warnings.