Skip to content

Conversation

@sim642
Copy link
Member

@sim642 sim642 commented Apr 14, 2022

This was an attempt to regenerate the benchmarks from #3 using a newer version of Klever etc. Seems that the Frama-C issue has been fixed: #3 (comment). Moreover, the generated benchmarks use a Linux 5.5 build base instead of 4.2.6 or 4.18.

Requires goblint/analyzer#688 to analyze with Goblint.

TODO

  • Is Goblint sound on them?
  • Is the amount of dead code expected from the unused model?
  • Are there even threads, races and locks to analyze?

@sim642 sim642 added the new benchmark New benchmark to analyze label Apr 14, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

new benchmark New benchmark to analyze

Projects

None yet

Development

Successfully merging this pull request may close these issues.

CPALockator's Linux device driver data race detection benchmarks

2 participants