Skip to content

Memory Leak Analysis#1127

Merged
michael-schwarz merged 13 commits intogoblint:masterfrom
mrstanb:memleak-analysis
Aug 16, 2023
Merged

Memory Leak Analysis#1127
michael-schwarz merged 13 commits intogoblint:masterfrom
mrstanb:memleak-analysis

Conversation

@mrstanb
Copy link
Copy Markdown
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

michael-schwarz
michael-schwarz reviewed Aug 5, 2023
View reviewed changes
michael-schwarz
michael-schwarz reviewed Aug 5, 2023
View reviewed changes
michael-schwarz
michael-schwarz reviewed Aug 5, 2023
View reviewed changes
github-advanced-security[bot]
github-advanced-security bot found potential problems Aug 8, 2023
View reviewed changes
michael-schwarz
michael-schwarz approved these changes Aug 9, 2023
View reviewed changes
Copy link
Copy Markdown
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 added feature sv-comp SV-COMP (analyses, results), witnesses labels Aug 9, 2023
sim642
sim642 approved these changes Aug 9, 2023
View reviewed changes
@sim642 sim642 added this to the v2.2.0 milestone Aug 9, 2023
@mrstanb
Copy link
Copy Markdown
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
Copy Markdown
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
Copy Markdown
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
@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 SV-COMP (analyses, results), witnesses

Projects

None yet

Milestone

v2.2.0

Development

Successfully merging this pull request may close these issues.

4 participants

@mrstanb @sim642 @michael-schwarz @github-advanced-security