Simmo Saan
Simmo Saan
Race warnings where MHP has a large created set are printed such that each thread ID component (in a history-based thread ID) is suffixed with a path to its creation...
In #1174 I made `pthread_join` invalidate its second argument with `w` instead of the default `r_deep; w_deep; s_deep`. Surprisingly, this caused test failures due to additional unknown pointer accesses if...
While working on #1069, there was some behavior which seemed suspect. Namely that `p->a = q->b` style assignments where `p` and `q` point to the same fresh blob should not...
## Example ### Program ```c #include #include int g, h; pthread_mutex_t A = PTHREAD_MUTEX_INITIALIZER; extern int *get(); void *t_fun(void *arg) { pthread_mutex_lock(&A); int *p = get(); *p = 3; //...
It would be good if our taint analysis tutorial also had a nice documentation page like the signs tutorial has. It is currently very difficult to solve individually without a...
> I don't think it's problematic, inside this domain the `ikind` is not stored and only used to compute the ranges: > > https://github.com/goblint/analyzer/blob/4d18300af5f6ae1b04bdbf29b29775af07fbc96c/src/cdomains/intDomain.ml#L2157 > > https://github.com/goblint/analyzer/blob/4d18300af5f6ae1b04bdbf29b29775af07fbc96c/src/cdomains/intDomain.ml#L1989 _Originally posted by...
Related to a couple of `*_unlocked` functions from the list, turns out there are `flockfile`, `ftrylockfile` and `funlockfile`, which treat a `FILE` as a mutex. No idea, if anyone uses...
The Android app has a feature to show a red X for tile positions which cannot be filled with remaining tiles. It would be nice of JCloisterZone also supported this....
JCloisterZone correctly shows the positions where a new tile can be placed, but occasionally hovering over one of them shows the tile in an invalid direction. If all the possible...
https://github.com/ocaml/opam-repository/pull/24493 reveals test failures on macos-homebrew: [goblint-cil.2.0.0.macos-homebrew.txt](https://github.com/goblint/cil/files/12698201/goblint-cil.2.0.0.macos-homebrew.txt) Namely: ``` - ------------ [418] CC="gcc-13" make testrungcc/builtin_object_size OPTIMIZE=1 ------------ - - [418] A regression test command failed: - CC="gcc-13" make testrungcc/builtin_object_size OPTIMIZE=1...