Simmo Saan

Float domain ill-typed program crash on concrat/Mirai-Source-Code

2

The following snippet, extracted from concrat/Mirai-Source-Code, crashes Goblint: ```c // PARAM: --enable ana.float.interval // Extracted from concrat/Mirai-Source-Code. extern int ( /* missing proto */ ceil)() ; int main() { int...

Atomic operations support

1

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: - [...

Spurious type-based races for deep accesses to unknown pointers

1

## 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...

Analysis coverage reports

3

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...

Precise `strdup`

6

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.