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.

Sign up for GitHub

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

Jump to bottom

Memory Leak Analysis #1127

Merged
merged 13 commits into from
Aug 16, 2023
Merged

Memory Leak Analysis #1127

merged 13 commits into from
Aug 16, 2023

Conversation

mrstanb
Copy link
Member

@mrstanb mrstanb commented Aug 4, 2023

This PR contains a first simple version of a memory leak analysis:

  • Should work for single-threaded programs provided that ana.malloc.unique_address_count is set to a value > 0
  • Currently uses a simple heuristic to warn for potential memory leaks whenever the program is multi-threaded

make test fails for test case 76/02 if one uses a comment //WARN on line 7 of this test case. The error message is:
Expected warn, but registered other
Because of this I've removed the //WARN from this test case for now

github-advanced-security[bot]
github-advanced-security bot found potential problems Aug 8, 2023
View reviewed changes
src/analyses/memLeak.ml Fixed Show resolved Hide resolved
michael-schwarz
michael-schwarz approved these changes Aug 9, 2023
View reviewed changes
Copy link
Member

@michael-schwarz michael-schwarz left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM!

sim642
sim642 approved these changes Aug 9, 2023
View reviewed changes
src/analyses/memLeak.ml Outdated Show resolved Hide resolved
@sim642 sim642 added this to the v2.2.0 milestone Aug 9, 2023
@mrstanb
Copy link
Member Author

mrstanb commented Aug 9, 2023

Feel free to merge.

I'll open a new PR to update the memLeak analysis with support for quick_exit as soon as #1135 is also ready and merged.

@mrstanb
Copy link
Member Author

mrstanb commented Aug 11, 2023

I'll open a new PR to update the memLeak analysis with support for quick_exit as soon as #1135 is also ready and merged.

Actually, I think it's unnecessary to open a new PR for this. I'll just update this one with a merge commit from master

@mrstanb
Copy link
Member Author

mrstanb commented Aug 11, 2023

Merged with master after #1135 was done. Added a regression test which now also covers a memory leak with quick_exit(). make test runs through fine with it.

@michael-schwarz michael-schwarz merged commit 69ee716 into goblint:master Aug 16, 2023
10 checks passed
@michael-schwarz michael-schwarz mentioned this pull request Oct 1, 2023
Closed
@sim642 sim642 mentioned this pull request Nov 24, 2023
Merged
sim642 added a commit to sim642/opam-repository that referenced this pull request Nov 24, 2023
@sim642
[new release] goblint (2.3.0)
34ad5a7 
CHANGES:

Functionally equivalent to Goblint in SV-COMP 2024.

* Add termination analysis for loops (goblint/analyzer#1093).
* Add memory out-of-bounds analysis (goblint/analyzer#1094, goblint/analyzer#1197).
* Add memory leak analysis (goblint/analyzer#1127, goblint/analyzer#1241, goblint/analyzer#1246).
* Add SV-COMP `termination`, `valid-memsafety` and `valid-memcleanup` properties support (goblint/analyzer#1220, goblint/analyzer#1228, goblint/analyzer#1201, goblint/analyzer#1199, goblint/analyzer#1259, goblint/analyzer#1262).
* Add YAML witness version 2.0 support (goblint/analyzer#1238, goblint/analyzer#1240, goblint/analyzer#1217, goblint/analyzer#1226, goblint/analyzer#1225, goblint/analyzer#1248).
* Add final warnings about unsound results (goblint/analyzer#1190, goblint/analyzer#1191).
* Add many library function specifications (goblint/analyzer#1167, goblint/analyzer#1174, goblint/analyzer#1203, goblint/analyzer#1205, goblint/analyzer#1212, goblint/analyzer#1220, goblint/analyzer#1239, goblint/analyzer#1242, goblint/analyzer#1244, goblint/analyzer#1254, goblint/analyzer#1269).
* Adapt automatic configuration tuning (goblint/analyzer#912, goblint/analyzer#921, goblint/analyzer#987, goblint/analyzer#1168, goblint/analyzer#1214, goblint/analyzer#1234).
nberth pushed a commit to nberth/opam-repository that referenced this pull request Jun 18, 2024
@sim642 @nberth
[new release] goblint (2.3.0)
8f8e773 
CHANGES:

Functionally equivalent to Goblint in SV-COMP 2024.

* Add termination analysis for loops (goblint/analyzer#1093).
* Add memory out-of-bounds analysis (goblint/analyzer#1094, goblint/analyzer#1197).
* Add memory leak analysis (goblint/analyzer#1127, goblint/analyzer#1241, goblint/analyzer#1246).
* Add SV-COMP `termination`, `valid-memsafety` and `valid-memcleanup` properties support (goblint/analyzer#1220, goblint/analyzer#1228, goblint/analyzer#1201, goblint/analyzer#1199, goblint/analyzer#1259, goblint/analyzer#1262).
* Add YAML witness version 2.0 support (goblint/analyzer#1238, goblint/analyzer#1240, goblint/analyzer#1217, goblint/analyzer#1226, goblint/analyzer#1225, goblint/analyzer#1248).
* Add final warnings about unsound results (goblint/analyzer#1190, goblint/analyzer#1191).
* Add many library function specifications (goblint/analyzer#1167, goblint/analyzer#1174, goblint/analyzer#1203, goblint/analyzer#1205, goblint/analyzer#1212, goblint/analyzer#1220, goblint/analyzer#1239, goblint/analyzer#1242, goblint/analyzer#1244, goblint/analyzer#1254, goblint/analyzer#1269).
* Adapt automatic configuration tuning (goblint/analyzer#912, goblint/analyzer#921, goblint/analyzer#987, goblint/analyzer#1168, goblint/analyzer#1214, goblint/analyzer#1234).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@sim642 sim642 sim642 approved these changes

@michael-schwarz michael-schwarz michael-schwarz approved these changes

Assignees
No one assigned
Labels
feature student-job sv-comp
Projects
None yet
Milestone
v2.2.0
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@mrstanb @sim642 @michael-schwarz