/* TAGS: */
/* VERIFY_OPTS: -o nofail:malloc */
/* CC_OPTS: */

// V: ok@safety                                    CC_OPT: -DCORRECT_MTX
// V: ok@local     V_OPT: --nontermination local   CC_OPT: -DCORRECT_MTX
// V: ok@global    V_OPT: --nontermination local   CC_OPT: -DCORRECT_MTX

// V: deadlock@safety        V_OPT: -o ignore:locking
// V: deadlock@local=!wait   V_OPT: --nontermination local,~mutex-wait -o ignore:locking  ERR: error trace: critical section
// V: deadlock@local=!crit   V_OPT: --nontermination local,~critical   -o ignore:locking  ERR: error trace: mutex lock
// V: deadlock@local=all     V_OPT: --nontermination local             -o ignore:locking  ERR: error trace: termsec check begin
// V: deadlock@global        V_OPT: --nontermination global            -o ignore:locking  ERR: error trace: .*

#include <pthread.h>
#include <thread>

int main() {
    pthread_mutex_t mtx;
    pthread_mutexattr_t mta;
    pthread_mutexattr_init( &mta );
    pthread_mutexattr_settype( &mta, PTHREAD_MUTEX_RECURSIVE );
    pthread_mutex_init( &mtx, &mta );

    int x = 0;

    std::thread t( [&] {
        pthread_mutex_lock( &mtx );
        pthread_mutex_lock( &mtx );
        x = 42;
        pthread_mutex_unlock( &mtx );
#ifdef CORRECT_MTX
        pthread_mutex_unlock( &mtx );
#endif
    } );

    for ( int a = 0; a != 42; ) {
        pthread_mutex_lock( &mtx );
        a = x;
        pthread_mutex_unlock( &mtx );
    }
    t.join();
}