Skip to content

Recursive mutex regression tests for creation locksets - #1928

Merged
michael-schwarz merged 2 commits into
goblint:masterfrom
dabund24:creation-lockset-recursive-mutex
Jan 23, 2026
Merged

Recursive mutex regression tests for creation locksets#1928
michael-schwarz merged 2 commits into
goblint:masterfrom
dabund24:creation-lockset-recursive-mutex

Conversation

@dabund24

Copy link
Copy Markdown
Member

As discussed here, recursive mutexes lead to some imprecise analysis results for the creation lockset analysis. This PR adds two regression tests in order to document this.

@michael-schwarz
michael-schwarz merged commit 94c3632 into goblint:master Jan 23, 2026
11 checks passed
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

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants