goblint / analyzer

Static analysis framework for C
https://goblint.in.tum.de
MIT License
160 stars 72 forks source link

Fix pthread mutex type from initializer on OSX #1416

Closed sim642 closed 2 months ago

sim642 commented 2 months ago

Fixes 71-doublelocking/19-default-init not passing in OSX CI.

OSX pthread_mutex_t doesn't have a .__data.__kind field where the mutex type is assigned on initialization. Rather there's a .__sig field with magic constants. We already hard-code an OSX constant for PTHREAD_MUTEX_RECURSIVE, so such hard-coding is not new: https://github.com/goblint/analyzer/blob/50f53042912062b5dcb028ed5b3ec0a6ac3d57f2/src/cdomain/value/cdomains/mutexAttrDomain.ml#L25 A cleaner (but also weirder) solution would be to extract actual values configure-style (a la CIL's Machdep).