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

Detect memory deallocation at offset from memory start #1139

Merged
merged 6 commits into from
Aug 22, 2023

Conversation

mrstanb
Copy link
Member

@mrstanb mrstanb commented Aug 18, 2023

This PR is supposed to improve Goblint's detection of invalid-free bugs by adding a check for memory deallocation which happens at an offset from the memory's start address instead of at the start address itself.

Added a few more regression test cases for this as well. make test runs through successfully

Cf. https://cwe.mitre.org/data/definitions/761.html

@sim642 sim642 added the sv-comp SV-COMP (analyses, results), witnesses label Aug 18, 2023
src/analyses/base.ml Outdated Show resolved Hide resolved
@sim642 sim642 added this to the v2.2.0 milestone Aug 22, 2023
@michael-schwarz michael-schwarz merged commit 1da8e97 into goblint:master Aug 22, 2023
9 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
feature student-job sv-comp SV-COMP (analyses, results), witnesses
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants