analyzer
analyzer copied to clipboard
goblint
Static analysis framework for C
We currently enable this everywhere, which leads to `volatile` and `extern` variables always having the value `T`. While this of course safe and makes sense when analyzing e.g. drivers, it...
This adds a Mutex-Meet-TID based privatization for Base. TODO: - [x] Tests - [ ] See if more duplication can be avoided between the relational and non-relational analysis During the...
`UpdateCil` updates IDs of statements (`sid`) and variables (`vid`), but not `compinfo` keys (`ckey`). I already wondered this in #598 but now here's concrete evidence that not updating them causes...
## Findings @michael-schwarz and I did some runs of Goblint (`master`) on the SQLite amalgamation, and investigated performance using `perf` and the [firefox-profiler](https://profiler.firefox.com/). We looked at the high run time...
When running the regression tests with `./scripts/update_suite.rb` on my system, multiple tests complain that the file `linux-headers/include/linux/compiler-gcc12.h` is missing. This persists even after running `make header`. I am using zsh,...
This WIP is the Munich idea for aborting. It's still far from polished, just thought I'd open the PR in case someone wants to take a look. TODOs: - [x]...
This pull requests builds on top of [my pull request about detection renamed local variables](https://github.com/goblint/analyzer/pull/731). It implements an algorithm, that can detect renamed functions and global variables on an incremental...
We should aim to support recursive mutexes more thoroughly: We could e.g. maintain an interval expressing how many times a recursive mutex is locked, or alternatively just maintain if it...
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...
Those are features we currently do not support yet, but it might be interesting to do so.