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

Race check in CBMC #8566

Open
Misasasa opened this issue Jan 14, 2025 · 0 comments
Open

Race check in CBMC #8566

Misasasa opened this issue Jan 14, 2025 · 0 comments

Comments

@Misasasa
Copy link

I find some old codes (up to February 2006) related to data races in race_check.cpp/h (which, I guess, perhaps implements the method in Bounded Model Checking of Concurrent Programs, CAV 2005). I also find an option "--race-check" to enable them. But the option seems not working. Could you please tell us whether it is still possible to enable race check in CBMC?

CBMC version: 5.67.0
Operating system: Ubuntu 24.04
Exact command line resulting in the issue: cbmc example.c --race-check
What behaviour did you expect: CBMC models and detects data races in the input program.
What happened instead: CBMC does not recognize the --race-check option.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant