Skip to content

Fix spurious overflow in pointer subtraction - #1909

Merged
sim642 merged 2 commits into
masterfrom
ptr-minus-speculating
Jan 16, 2026
Merged

sim642 merged 2 commits into
masterfrom
ptr-minus-speculating

Conversation

@sim642

@sim642 sim642 commented Jan 16, 2026

Copy link
Copy Markdown
Member

Found by @karoliineh during dashboard evaluation.

@sim642 sim642 added this to the SV-COMP 2027 milestone Jan 16, 2026
@sim642
sim642 requested a review from karoliineh January 16, 2026 12:47
@sim642 sim642 added bug sv-comp SV-COMP (analyses, results), witnesses precision labels Jan 16, 2026

@karoliineh karoliineh left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

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

Fixes the issue in the affected benchmarks that I manually checked.

@sim642
sim642 merged commit db15e2e into master Jan 16, 2026
19 checks passed
@sim642
sim642 deleted the ptr-minus-speculating branch January 16, 2026 14:17
avsm pushed a commit to ocaml/opam-repository that referenced this pull request Jun 15, 2026
CHANGES:

* Add new may-happen-in-parallel analyses (goblint/analyzer#1805, goblint/analyzer#1865, goblint/analyzer#1913, goblint/analyzer#1928).
* Add Open Verification Dashboard checks output (goblint/analyzer#1838, goblint/analyzer#1929).
* Add negative bitwise shift warnings (goblint/analyzer#1637, goblint/analyzer#1989).
* Add missing function declaration warnings (goblint/analyzer#1911).
* Improve overflow warnings (goblint/analyzer#1894, goblint/analyzer#1895, goblint/analyzer#1896, goblint/analyzer#1905).
* Fix spurious overflow checks (goblint/analyzer#1767, goblint/analyzer#1909, goblint/analyzer#1910, goblint/analyzer#1932, goblint/analyzer#2022).
* Fix missing overflow and out-of-bounds checks (goblint/analyzer#1935, goblint/analyzer#2017, goblint/analyzer#2029).
* Optimize base analysis domain using Patricia trees (goblint/analyzer#2002, goblint/analyzer#2015).
* Optimize field offset calculations (goblint/analyzer#1964, goblint/analyzer#1973, goblint/analyzer#1974).
* Optimize non-incremental top-down solver (goblint/analyzer#1566, goblint/analyzer#1972).
* Add OCaml 5.5 support (goblint/analyzer#2006, goblint/analyzer#2010).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

bug precision sv-comp SV-COMP (analyses, results), witnesses

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants