analyzer
analyzer copied to clipboard
Thread analysis crashes with musl
Version 2.0.0 release on opam reveals the following thread analysis crashes on alpine, which notably uses musl instead of glibc:
- [ ] 10/25 tid-array-malloc
- [ ] 10/26 tid-array-malloc-free
Thus, I have disabled Goblint on alpine.
The crash itself is
Fatal error: exception Goblint_lib.SetDomain.Unsupported("elements on `Top")
but the root cause is the warning
[Warning][Unknown] size of error: abstract type (tests/regression/10-synch/25-tid-array-malloc.c:12:5-12:48
The issue is that these tests use sizeof(pthread_t)
, but in musl headers pthread_t
is defined as an abstract struct, so its size is unknown.
in musl headers
pthread_t
is defined as an abstract struct, so its size is unknown.
This is actually wrong because otherwise you couldn't even have static pthread_t
arrays. So really it's a pointer to an abstract struct:
typedef struct __pthread * pthread_t;
The size of a pointer is well-known so that's not the issue, but I guess for some reason we're trying to get the size of the pointed type as well even though it should be irrelevant.