Reachable error in pthread-ext/41_FreeBSD_abd_kbd_sliced

[schuessf]

The program pthread-ext/41_FreeBSD_abd_kbd_sliced is labeled as true. However there should be a feasible counterexample trace (which Ultimate Automizer also found). One thread can simply call akbd_read_char(1) and therefore execute the trace:

__VERIFIER_atomic_acquire();
COND = 0;
__VERIFIER_atomic_release();
assume_abort_if_not(COND);
__VERIFIER_atomic_acquire();
if(!(COND)) { goto ERROR; }

For this error trace to be feasible we need to set COND to 1 before the assume_abort_if_not and back to 0 after it. This can be achieved, if other threads call adb_kbd_receive_packet() and akbd_read_char(1) respectivitely (since the mutex is not locked there). Therefore it seems that this example should be labeled as false (unreach-call).