SV-COMP evaluation feedback

[vesalvojdani]

Overall, locksmith works very well as a verification tool: there are only two unsoundness issues. The first is just because locksmith does not register accesses on arguments to scanf. Since locksmith warns that this is an unknown function, I made locksmith answer "unknown" in this case, so this is not counted as a wrong verdict.

The only real unsoundness issue occurs on a benchmark where two distinct mutexes are chosen non-deterministically. One can simplify the issue to the following example, which has no branching:

#include <pthread.h>

int myglobal;
pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;

void *t_fun(void *arg) {
  pthread_mutex_lock(&mutex1);
  myglobal=myglobal+1;
  pthread_mutex_unlock(&mutex1);
  return NULL;
}

int main(void) {
  pthread_t id;
  pthread_mutex_t *m;

  m = &mutex1;
  m = &mutex2;

  pthread_create(&id, NULL, t_fun, NULL);

  pthread_mutex_lock(m);
  myglobal=myglobal+1;
  pthread_mutex_unlock(m);

  pthread_join (id, NULL);
  return 0;
}

Locksmith does not complain about the above program in its default configuration and I tried various flow-sensitivity options, but the result is still the same. It is as if both mutex1 and mutex2 is seen to be flowing to m. I wonder if there is some flag that I'm overlooking here or is it a real bug?