Showing error 2206

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


Source:

1216    for (i = 0; i < iCheck; i++) {
1217        if (0 != (err = pthread_create(&checkPool[i], ((void *)0), &checkThread,
1218                                       ((void *)0)))) {
1219            fprintf(stderr, "Error [%d] found creating check thread.\n", err);
1220            exit(-1);
1221        }
1222    }
1223    for (i = 0; i < iSet; i++) {
1224        if (0 != (err = pthread_join(setPool[i], ((void *)0)))) {
1225            fprintf(stderr, "pthread join error: %d\n", err);
1226            exit(-1);
1227        }
1228    }
1229    for (i = 0; i < iCheck; i++) {
1230        if (0 != (err = pthread_join(checkPool[i], ((void *)0)))) {
1231            fprintf(stderr, "pthread join error: %d\n", err);
1232            exit(-1);
1233        }
1234    }
1235    return 0;
1236}
1237void *setThread(void *param) {
1238    a = 1;
1239    b = -1;
1240    return ((void *)0);
1241}
1242void *checkThread(void *param) {
1243    if (! ((a == 0 && b == 0) || (a == 1 && b == -1))) {
1244        fprintf(stderr, "Bug found!\n");
1245        goto ERROR;
1246        ERROR:
1247          ;
1248    }
1249    return ((void *)0);
1250}
Show full sources