Simmo Saan

I tried with the exact executable from the verifier archive (SHA-256 below) and I still gives the `unknown` answer: ``` simmo@goblint-new:/mnt/goblint-svcomp/sv-comp/goblint$ sha256sum ./asd/goblint/goblint 16574d3cacb6ab22b29fada00cdeecc14c74706cf6d90526e4068329616d3618 ./asd/goblint/goblint simmo@goblint-new:/mnt/goblint-svcomp/sv-comp/goblint$ ./asd/goblint/goblint --conf conf/svcomp21.json --sets...

Hmm yeah, it does happen with `pals_opt-floodmax.5.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c` on the archive build, so there is _some_ consistency. In the supposedly final results (linked in Slack) there's one more case: `seq-mthreaded-reduced/pals_opt-floodmax.4.3.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c`. It...

Fixed by #809 and #827.

That support is questionable at best: https://github.com/goblint/analyzer/blob/179c8b94ae0c801683d00fbf89f14e7e81223091/src/analyses/mutexAnalysis.ml#L165-L171 Whether a memory access is a read or write (argument `w`) has nothing to do with whether we're holding a read or write...

That is also reflected by this existing regression test: https://github.com/goblint/analyzer/blob/179c8b94ae0c801683d00fbf89f14e7e81223091/tests/regression/04-mutex/41-pt_rwlock.c#L9-L24 Writer-reader pairs do mutually exclude each other, so there should be no race, but we report one because our assumption...

Now this seems tricky because we'll somehow have to keep track of the casts and do something special. We already perform a cast from `char` to `int` at that write,...

This point came up again in a discussion with @vesalvojdani regarding all the things that addresses and their offsets, including #816. It seems that our addresses need to be typed.

04/71 memset_direct_rc is just because the the fortified version replaces `memset` with a macro that calls an inline function instead, so the race location ends up being there, not where...

Also what wasn't implemented was the path-sensitive analysis based loop unrolling by counting iterations in the domain. Not sure if that deserves a separate issue, but I still think that...

## Compiling Compiling the regression tests is definitely a sanity check we should have. This was also witnessed by having to add a missing `#include ` to 160 tests using...