Simmo Saan

Optimize CFG representation

13

Split CFG hashtables per function throughout, not just for the duration of connectedness checking (like in #603). This should speed up analogous lookups during transfer functions as well (which use...

In the chrony interactive story, `compile_commands.json` would normally be in the chrony-4.2 git submodule, making it impossible to version the compilation database in our bench repository for better reproducibility. Compilation...

Detect calls of thread-unsafe functions as races

1

Under "Thread-safe functions" of [pthreads man page](https://man7.org/linux/man-pages/man7/pthreads.7.html), it says the following: > A thread-safe function is one that can be safely (i.e., it will deliver the same results regardless of...

Structs sets domain causes many incomparable comparisons on zstd

1

Out of curiosity I wanted to try the `sets` domain for base structs (from #419) on zstd, because with simple structs we lose the relationship between its thread pool functions...

I continued looking at chrony after #712 and found another little bit of unsoundness: the callback function `name_resolve_handler` is never called. The problem is that at an intermediate level of...

While looking at chrony and how it uses a `pipe` to return results from a pthread thread (which is a bit weird in itself), I remembered the pre-threads way of...

Fix regression tests with fortify source

1

Using `_FORTIFY_SOURCE` (and the optimization required for it), regression tests can be run with: ```console gobopt='--set pre.cppflags[+] -D_FORTIFY_SOURCE=2 --set pre.cppflags[+] -O3' ./scripts/update_suite.rb ``` I used these options to debug MacOS...

I happened upon [GCC's common function attributes](https://gcc.gnu.org/onlinedocs/gcc/Common-Function-Attributes.html) and noticed many that we could (and should) support. For example to allow more flexible specifications for `LibraryFunctions` or malloc wrappers. Clang also...

Suppose I have done a batch analysis and saved the results using `incremental.save`. Then currently there's no way to start server mode and load that incremental data I already have....

Adds support for Klever/LDV specific concurrency safety model functions as described in https://github.com/goblint/bench/issues/3#issuecomment-1056675513. Needed to analyze https://github.com/goblint/bench/pull/27.