analyzer
analyzer copied to clipboard
goblint
Static analysis framework for C
## 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...
Would be good to have this sooner rather than later. Goblint can't analyze Juliet suite race detection stuff because they use some wrappers that end up creating pointers to structs...
SV-Comp '21 revealed a few example programs where we do not reach the fixpoint: - [ ] c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v%2Bcfa-reducer.yml - [ ] c/seq-mthreaded-reduced/pals_opt-floodmax.5.1.ufo.BOUNDED-10.pals.c.v%2Bnlh-reducer.yml - [ ] c/seq-mthreaded-reduced/pals_opt-floodmax.5.2.ufo.UNBOUNDED.pals.c.v%2Bcfa-reducer.yml - [ ] c/seq-mthreaded-reduced/pals_opt-floodmax.5.3.ufo.BOUNDED-10.pals.c.v%2Bnlh-reducer.yml...
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`...
Values that are physically equal or, for `HConsed` have the same tag, are also `leq`. We should exploit this by implementing a short-circuiting version of `leq` for `HConsed`.
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,...
### Problem: Precision loss in combine with partial contexts When analyzing functions with partial contexts, the final state of a function `f` thus can contain abstract values joined over multiple...
There is no reason we cannot also make use of MHP in the non-relational Mutex-Meet privatization. This should be added such that we can, e.g. profit from MHP information to...
This draft PR introduces an analysis for affine equalities (ref: [Michael Karr , 1976](https://scholar.google.com/scholar_url?url=https://idp.springer.com/authorize/casa%3Fredirect_uri%3Dhttps://link.springer.com/content/pdf/10.1007/BF00268497.pdf%26casa_token%3DjHkKNvRPTY4AAAAA:yxzkcPFZP1RWxLZY-TWAg7cO8EfC0Txc78-CTZiDMFnyvkXp54p3s6RHEnxG0Auh7NRZELlImjxkZTat&hl=en&sa=T&oi=gsb-gga&ct=res&cd=0&d=14162577617566575899&ei=444CYu9y-pXL1g-ynpHACg&scisig=AAGBfm24cgr8mbazZ4npHDMjTnSTHqGDUA)) that can be run independently from the already existing apron analyses. Abstract states in the newly...
As discussed in #731 the rename mapping introduced for detecting renames of local variables or formal parameters in the AST comparison can easily be passed through to the cfg comparison....
