source: CIVL/examples/pthread/stateful01_false.cvl@ 325d439

/**
* This is a translation of a Pthread program from 
* the Pthread benchmarks of SV-COMP 2014.
* https://svn.sosy-lab.org/software/sv-benchmarks/tags/svcomp14/
*
* Command line execution:
* civl verify stateful01_false.cvl -min
*/

#include <civlc.h>
#include "pthread.cvh"

pthread_mutex_t ma, mb;
int data1, data2;

void *thread1(void*arg)
{  
  pthread_mutex_lock(&ma);
  data1++;
  pthread_mutex_unlock(&ma);

  pthread_mutex_lock(&ma);
  data2++;
  pthread_mutex_unlock(&ma);
}

void *thread2(void*arg)
{  
  pthread_mutex_lock(&ma);
  data1+=5;
  pthread_mutex_unlock(&ma);

  pthread_mutex_lock(&ma);
  data2-=6;
  pthread_mutex_unlock(&ma);
}

void main()
{
  pthread_t  t1, t2;

  pthread_mutex_init(&ma, 0);
  pthread_mutex_init(&mb, 0);

  data1 = 10;
  data2 = 10;

  pthread_create(&t1, 0, thread1, 0);
  pthread_create(&t2, 0, thread2, 0);
  
  pthread_join(t1, 0);
  pthread_join(t2, 0);

  if (data1==16 && data2==5)
  {
    $assert($false);
  }
}