Simmo Saan
Simmo Saan
This issue serves as a WIP place to collect issues and workarounds for different compilation database generators we have encounted. ## compiledb 1. Doesn't properly escape `-D` argument values (https://github.com/goblint/bench/issues/8#issuecomment-1017538298,...
In https://github.com/goblint/analyzer/pull/655/commits/3124e376b93054e742b6cd302e5c71bf8ccf2949 @michael-schwarz added a deadlock example, where a thread forgets to unlock a mutex before returning. Then the joining thread deadlocks trying to lock it. Detecting this is more...
With the revival of deadlock analysis (#655), it becomes more and more important that we handle behavior specific to mutex types. Via [`pthread_mutexattr_settype`](https://linux.die.net/man/3/pthread_mutexattr_settype) there are the following possibilities: - [...
In the context of interactive analysis, minimizing the wall time of preprocessing and parsing of large projects with many files would be beneficial. But this would also be useful non-incrementally....
In some cases it might be necessary to do manual incremental restarting not by a global variable name, but a type name. In particular, the access analysis has some type-based...
In https://github.com/goblint/analyzer/pull/597#discussion_r810470622, it came up again that we have this weird `__BLOCKS__` undefine: https://github.com/goblint/analyzer/blob/b11a60cd5896b41f9e0c4847825d21f045dc6cc1/src/maingoblint.ml#L161-L163 This is something MacOS specific. So the question is whether it's still required for some reason...
To be done after #391 is merged. - [x] Unmarshaling etc should be done outside (by `Control`?) - [x] Finding nodes to destabilize due to change should be done outside...
This issue appeared in https://github.com/goblint/analyzer/pull/542#issuecomment-1023077417, but previously happened to be accidentally hidden by some hashtable having keys stored and iterated in a different order. If the old function had no...
### Program Consider the following program: ```c #include typedef struct { int x; } a; int main() { a z; a *y = &z; int *m = &y->x; // {&z.x}...
This is an attempt (or two) to generalize the reluctant function return node destabilization during incremental loading to general use in TD3. This was discussed briefly during GobCon, but the...