analyzer
analyzer copied to clipboard
goblint
Static analysis framework for C
There are multiple families of atomic operations: - [ ] GCC `__sync` builtins: https://gcc.gnu.org/onlinedocs/gcc/_005f_005fsync-Builtins.html. - [ ] C11: https://en.cppreference.com/w/c/thread#Atomic_operations. There are three aspects in which to improve precision: - [...
## Example ### Program ```c // PARAM: --set lib.activated[+] zlib #include #include void *t_fun(void *arg) { z_stream stream; inflateInit2(&stream, 32 + 15); return NULL; } int main(void) { pthread_t id;...
## Problem ```console ./goblint ../goblint-bench/concrat/AirConnect/main.c -v --conf conf/examples/large-program.json ``` eventually terminates with ``` cputime walltime allocated count Default 394.815s 395.628s 522171.44MB 1× preprocess 0.055s 0.053s 0.02MB 1× FrontC 0.147s 0.149s...
Library activations (#1028) won't be precise until all of the old-style things are converted to new ones in appropriate groups: https://github.com/goblint/analyzer/blob/bcb4de29e22885570ba82f7ec9cee2e661854b7a/src/analyses/libraryFunctions.ml#L359-L400 https://github.com/goblint/analyzer/blob/bcb4de29e22885570ba82f7ec9cee2e661854b7a/src/analyses/libraryFunctions.ml#L500-L980 _Originally posted by @sim642 in https://github.com/goblint/analyzer/pull/996#discussion_r1143067617_
In large programs (like zstd), it's rather inconvenient to check abstract states using g2html, etc, because it takes forever to produce that additional output on top of the already long...
In larger programs and real-world projects it's often difficult to know whether a certain part of code was actually analyzed or not. Dead code warnings provide only partial information because...
Currently `strdup` (and `strndup`) return an unknown pointer, which can make things very imprecise. Instead we should: - [ ] Return a pointer to freshly allocated memory, the same way...
Suppose: ```c struct S { char* f; char* g; }; ``` If an access to type suffix `(char*)` races with an access to prefix `(struct S)`, then this is reported...
#800 and #1073 add multiplicity tracking for recursive mutexes. Maybe we could just reuse those abstract counters for semaphores as well.
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...