analyzer icon indicating copy to clipboard operation
analyzer copied to clipboard

Thread analysis crashes with musl

Open sim642 opened this issue 2 years ago • 1 comments

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.

sim642 avatar Aug 18 '22 14:08 sim642

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.

sim642 avatar Aug 19 '22 09:08 sim642