Showing error 2192

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: pthread/indexer_safe.i
Line in file: 2181
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

2151    tab[h] = new_val;
2152    ret_val = 1;
2153  }
2154
2155  pthread_mutex_unlock(&cas_mutex[h]);
2156
2157
2158  return ret_val;
2159}
2160
2161
2162
2163void * thread_routine(void * arg)
2164{
2165  int tid;
2166  int m = 0, w, h;
2167  tid = *((int *)arg);
2168
2169  while(1){
2170    if ( m < 4 ){
2171      w = (++m) * 11 + tid;
2172    }
2173    else{
2174      pthread_exit(((void *)0));
2175    }
2176
2177    h = (w * 7) % 128;
2178
2179    if (h<0)
2180    {
2181      ERROR: goto ERROR;
2182      ;
2183    }
2184
2185    while ( cas(table, h, 0, w) == 0){
2186      h = (h+1) % 128;
2187    }
2188  }
2189
2190}
2191
Show full sources
↑