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.

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

threadAnalysis: Only add to set of must-joined threads if argument to pthread_join evaluates to a singleton #1230

Merged
merged 2 commits into from
Nov 2, 2023

Conversation

michael-schwarz
Copy link
Member

The analysis added all unique threads in the points-to-set of the argument to pthread_join to the set of must-joined threads.
This is wrong, as only one of those is joined at runtime, so only if the set is singleton and the thread is unique can it be added.

Closes #1223

@michael-schwarz michael-schwarz added unsound sv-comp SV-COMP (analyses, results), witnesses labels Nov 1, 2023
@michael-schwarz michael-schwarz added this to the SV-COMP 2024 milestone Nov 1, 2023
@michael-schwarz
Copy link
Member Author

The failure of semgrep is unrelated.

@sim642 sim642 added the bug label Nov 2, 2023
@michael-schwarz michael-schwarz merged commit 808e91d into master Nov 2, 2023
@michael-schwarz michael-schwarz deleted the issue_1223 branch November 2, 2023 09:05
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug sv-comp SV-COMP (analyses, results), witnesses unsound
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Old thread analysis is unsound w.r.t. joins
2 participants