-
Notifications
You must be signed in to change notification settings - Fork 76
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
Experiment with path- and context-sensitivity for memLeak analysis #1234
Conversation
When being fully path- & context-sensitive, we succeed on 22 additional tasks. |
We get strictly better with each of these config options, so it seems clear we would want them. |
To facilitate development and get accurate pre-runs, I'd propose merging this now, so we don't have multiple PRs floating around. |
Quick question @sim642: I saw you specify |
It's a config I copied and adapted on the This PR doesn't even change |
Ok, thanks! Are you merging master back into
No, I think it makes sense to have it path-sensitive by default. |
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).
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).
I'll use this issue to document some of the steps towards coming up with a good config for sv-comp.
Machine Config
Results without any additional path- & context-sensitivity:
Results with full path- & context-sensitivity:
Results with full path- & context-sensitivity & unique count of 5:
Results with full path- & context-sensitivity & unique count of 5 & fix for #1235 :