analyzer
analyzer copied to clipboard
goblint
Static analysis framework for C
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,...
Using solver `wpoint`, two functions in one of the region tests are dead (but should not be): ~~~ Testing 09/23 regions/evilcollapse_rc Status: 3 (verify) ... - Fixpoint not reached at...
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...
Akin to our list of `malloc_wrappers` we should have `thread_create_wrappers` to generate better thread ids when all thread creations happen through a helper function wrapping `pthread_create`. This may, e.g. happen...
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: - [...
Simmo fixed some soundness issues (#106) that arise when the region analysis is executed with symbolic equality and field-sensitive refinement for all benchmarks. Previously, these flags were only turned on...
@jerhard and I were toying around with this idea a week or so ago, so I thought I'd write down some of our thoughts so they don't get lost. The...
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....
With #577 and #563 now merged, we now have the ability to unroll **all** loops **k** times and **all** arrays **l** times. Often, just unrolling everything will be expensive though...
Currently, the partitioned array domain is ~~~OCaml module Expp = ExpDomain module Base = Lattice.Prod3 (Val) (Val) (Val) include Lattice.ProdSimple(Expp) (Base) ~~~ with the additional understanding that the first component...