Simmo Saan
Simmo Saan
While debugging some benchmark programs, I noticed they themselves contain silly bugs: 1. Forgetting to unlock a mutex (e.g. at early return), which makes any following call of the function...
## Problem Our analysis of zstd ends up with unexpectedly many unknown pointers due to the following sequence of coincidences. ### Thread pool and its queue In zstd's `POOL_create_advanced`, the...
Races-as-reachability tests in 28-race_reach have TODO assertions which we currently cannot prove: - [ ] **22-deref_read_racefree.c** Global `q` may still point to initial `NULL` in addition to `&data` in `main`...
See https://github.com/goblint/analyzer/pull/609#issuecomment-1057333884 and the following comments. Special care should be taken of `GVarDecl`s that also have corresponding `GFun`s. The CIL invariant is that if they refer to the same function,...
As pointed out in https://github.com/goblint/analyzer/pull/770#discussion_r912977915, the expRelation analysis makes some claims about expressions containing arithmetic which may overflow. Depending on the configuration, we might not want it to make definite...
During benchmarking I found out that some base privatizations can be unsound during witness validation. I've added the following skipped test: https://github.com/goblint/analyzer/blob/e934d115271b7ae4b15e2d25edcf5e22dbcdb7ca/tests/regression/56-witness/04-base-priv-sync-prune.c. The invariant `g == 2` should definitely fail,...
Problem pointed out here: https://github.com/goblint/analyzer/pull/745#discussion_r883607234. > Good point, I didn't think about it here, but I think there's not much to do about it either. On the witness generation side,...
In https://github.com/goblint/analyzer/pull/737#discussion_r878862538 it became even more apparent that we have multiple must-equality analyses, some of which are not in regular use: 1. var_eq analysis is the one we regularly use,...
**The conclusion is to use Read the Docs but documenting into `docs` directory of this repository in Markdown.** ### Ideas for tutorial-style documentation - [x] Printing using `Pretty` - [x]...
## Problem Infamously, our `varinfo`s for dynamically allocated memory are created with `void` type, because at the point of `malloc`/etc. we don't yet know, which type the values assigned to...