/**
* 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 stack_true.cvl
*/

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

$input int SIZE;

_Bool TRUE = 1;
_Bool FALSE = 0;
int SIZE = 5;
int OVERFLOW = -1;
int UNDERFLOW = -2;

static int top=0;
static unsigned int arr[SIZE];
pthread_mutex_t m;
_Bool flag=FALSE;

void error(void) 
{ 
  $assert($false);
}

void inc_top(void)
{
  top++;
}

void dec_top(void)
{
  top--;
}

int get_top(void)
{
  return top;
}

int stack_empty(void)
{
  (top==0) ? TRUE : FALSE; 
}

int push(unsigned int *stack, int x)
{
  if (top==SIZE) 
  {
    printf("stack overflow\n");
    return OVERFLOW;
  } 
  else 
  {
    stack[get_top()] = x;
    inc_top();
  }
  return 0;
}

int pop(unsigned int *stack)
{
  if (top==0) 
  {
    printf("stack underflow\n");	
    return UNDERFLOW;
  } 
  else 
  {
    dec_top();
    return stack[get_top()];  
  }
  return 0;
}

void *t1(void*arg) 
{
  int i;
  unsigned int tmp;

  for(i=0; i<SIZE; i++)
  {
    pthread_mutex_lock(&m);   
    tmp = 1%SIZE;
    int tmp1 = push(arr,tmp);
    if (tmp1==OVERFLOW)
      error();
    pthread_mutex_unlock(&m);
  }
  return NULL;
}

void *t2(void*arg) 
{
  int i;

  for(i=0; i<SIZE; i++)
  {
    pthread_mutex_lock(&m);
    if (top>0)
    {   
      int tmp = pop(arr);
      if (tmp==UNDERFLOW)
        error();
    }    
    pthread_mutex_unlock(&m);
  }
  return NULL;
}


void main() 
{
  pthread_t id1, id2;

  pthread_mutex_init(&m, 0);

  pthread_create(&id1, NULL, t1, NULL);
  pthread_create(&id2, NULL, t2, NULL);

  pthread_join(id1, NULL);
  pthread_join(id2, NULL);
}