Skip to content

Conversation

@sim642
Copy link
Member

@sim642 sim642 commented Nov 5, 2025

This is on top of #1862 just to test on those regression test as well.

This is a quick attempt at fixing my long-time frustration with the useAfterFree analysis (there are also others).

We already have a very established access analysis which emits events for everything that is being accessed. Since it forms the basis of race analysis, it has gone through a lot of testing and iterations to make it correct.

So, the useAfterFree analysis should just use these events instead of (incorrectly) duplicating the logic of what's being accessed.
It seems to pass all of our regression tests, but appears to avoid the Juliet imprecision of #1861.

TODO

  • Distinguish access kinds again.
  • sv-benchmarks runs.

Instead of (incorrectly) duplicating the logic of what's being accessed.
@sim642 sim642 added cleanup Refactoring, clean-up bug unsound sv-comp SV-COMP (analyses, results), witnesses labels Nov 5, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

bug cleanup Refactoring, clean-up sv-comp SV-COMP (analyses, results), witnesses unsound

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants