c - 为什么在传递函数“pthread_create()”后变量“sum”的值会发生变化？

Question

我声明了一个变体sum并初始化为0，然后通过函数将它传递给func()函数pthread_create()。我没想到的是变体sum不再等于0（如您所见，函数assert()失败了）。我的 ubuntu 是 16.04.4 LTS。

直接用gcc编译就可以了， cbmc报错。

static void * func(void * arg)
{
  double *sum = (double *)arg;

  assert(*sum == 0.0);  //failed in CBMC
  return ((void *) 0);
}

int main(){

  double sum=0.0;
  pthread_t thr1;

  pthread_create(&thr1, NULL, &func, (void *)&sum );
  pthread_join(thr1, NULL);

  printf("sum = %f\n", sum);
  assert(sum == 0.0);   //successful in CBMC

  return 0;
}

以下是CBMC报告的警告：

State 70 file pthreads4.c line 24 function main thread 1
----------------------------------------------------
  arg=&sum!0@1 (0000010000000000000000000000000000000000000000000000000000000000)

State 71 file pthreads4.c line 12 function func thread 1
----------------------------------------------------
  sum=((double *)NULL) (0000000000000000000000000000000000000000000000000000000000000000)

State 72 file pthreads4.c line 12 function func thread 1
----------------------------------------------------
  sum=&sum!0@1 (0000010000000000000000000000000000000000000000000000000000000000)

Violated property:
  file pthreads4.c line 14 function func
  assertion *sum == 0
  IEEE_FLOAT_EQUAL(*sum, (double)0)

VERIFICATION FAILED

标签： cpthreadsverification