Opened 4 weeks ago

Closed 5 days ago

#83 closed defect (fixed)

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

Reported by: imartisko Owned by: mornfall
Priority: major Milestone: 4.5
Component: other Keywords:
Cc: jamartis@…, kdudka@…, lzaoral@…

Description

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

Attachments (1)

main.c (877 bytes) - added by imartisko 4 weeks ago.

Download all attachments as: .zip

Change History (3)

Changed 4 weeks ago by imartisko

Attachment: main.c added

comment:1 Changed 4 weeks ago by 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?

comment:2 Changed 5 days ago by mornfall

Resolution: fixed
Status: newclosed

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.

Note: See TracTickets for help on using tickets.