ex7-v5.c

ex7-v5.c

//SAFE
int sum, sum2=0;

int func1(int a, int b)
{
  sum = 1;
  if(a < 0){
  	a = b + a; //critical
  	return a;
  }
  else 
  	return b;
}


int func2(int a, int b)
{
  return sum+2;
}

void main()
{
  int a = nondet();
  int b = nondet();
  __VERIFIER_assume(a > -10 && a < 10);
  __VERIFIER_assume(b > -10 && b < 10);
  int c = a;
  int d = b;
  int p=0, q=0;

  if (a + b >= 0) {
  	p = func1(a, b) + func2(a, b);
  	q = func1(c, d) + func2(c, d);
  }	
  assert(p == q); //SAFE
}