Divince check: false negative when using NULL as the first argument of the pthread_create()

[imartisko]

Hello,
when checking the attached file, divine check returns different results based on which branch of the IF condition is executed. If the TRUE branch is executed, the check reports no errors, if the ELSE branch is executed, an error is correctly reported (the malloc/write/read threads are not synchronized). The only difference between the branches is, whether a proper value or NULL is passed as the first argument of the pthread_create() function.

Thanks,
Jakub

[imartisko]

This happens with:

DIVINE 4, version 4.3.6+d01d5d4322f

version: 4.3.6+d01d5d4322f
source sha: 87b538a6be2afb1208992f7d03ee14bb2e361073
runtime sha: 8ab4ed728c0501c33689859bf5507fc2b553ee24
build date: 2019-09-09, 16:38 UTC
build type: RelWithDebInfo?

[mornfall]

What happens is that pthread_create in dios returns EINVAL in this case, without starting the thread. The spec does not mention that EINVAL could arise this way, though in many other places that would be correct behaviour. I am turning this into a hard failure, since the code crashes at least on Linux and OpenBSD.
In other words, should be fixed in next.