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

Final errors about unsound results #1190

Closed
5 of 6 tasks
sim642 opened this issue Sep 26, 2023 · 0 comments · Fixed by #1191
Closed
5 of 6 tasks

Final errors about unsound results #1190

sim642 opened this issue Sep 26, 2023 · 0 comments · Fixed by #1191
Assignees
@sim642
Labels
benchmarking feature unsound-usability usability
Milestone
v2.3.0

Comments

@sim642
Copy link
Member

sim642 commented Sep 26, 2023 •
edited
Loading

Recent experiences have shown that it's too easy to miss key messages about unsoundness on real-world projects with lots of output. This is made worse by confs that disable most output, making such problems impossible to notice.

The solution would be to print additional errors after all other messages when some of the following have occurred:

  • Fixpoint not reached.
  • Function definition missing.
  • Both branches dead.
  • No suitable function to call.
  • ASM ignored.
  • ...?

By making these errors last in the output, they will be visible on the terminal after such long analysis finishes and be more likely to be noticed.
Also they should not be suppressed by options to make sure we always notice invalid results before using them in papers.
@sim642 sim642 self-assigned this Sep 26, 2023
sim642 added a commit that referenced this issue Sep 26, 2023
@sim642
Add final messages (issue #1190)
0caab0f
@sim642 sim642 mentioned this issue Sep 26, 2023
Merged
@sim642 sim642 added this to the v2.3.0 milestone Sep 26, 2023
@michael-schwarz michael-schwarz mentioned this issue Oct 16, 2023
Merged
@sim642 sim642 mentioned this issue Nov 24, 2023
Merged
sim642 added a commit to sim642/opam-repository that referenced this issue 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 issue 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
Assignees

@sim642 sim642

Labels
benchmarking feature unsound-usability usability
Projects
None yet
Milestone
v2.3.0
Development

Successfully merging a pull request may close this issue.

Add final messages about unsound results goblint/analyzer
1 participant
@sim642