Showing error 1468

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

Source: 

  1extern int __VERIFIER_nondet_int();
  2int main()
  3{
  4    int p1 = __VERIFIER_nondet_int();  // condition variable
  5    int lk1; // lock variable
  6
  7    int p2 = __VERIFIER_nondet_int();  // condition variable
  8    int lk2; // lock variable
  9
 10    int p3 = __VERIFIER_nondet_int();  // condition variable
 11    int lk3; // lock variable
 12
 13    int p4 = __VERIFIER_nondet_int();  // condition variable
 14    int lk4; // lock variable
 15
 16    int p5 = __VERIFIER_nondet_int();  // condition variable
 17    int lk5; // lock variable
 18
 19    int p6 = __VERIFIER_nondet_int();  // condition variable
 20    int lk6; // lock variable
 21
 22    int p7 = __VERIFIER_nondet_int();  // condition variable
 23    int lk7; // lock variable
 24
 25    int p8 = __VERIFIER_nondet_int();  // condition variable
 26    int lk8; // lock variable
 27
 28
 29    int cond;
 30
 31    while(1) {
 32        cond = __VERIFIER_nondet_int();
 33        if (cond == 0) {
 34            goto out;
 35        } else {}
 36        lk1 = 0; // initially lock is open
 37
 38        lk2 = 0; // initially lock is open
 39
 40        lk3 = 0; // initially lock is open
 41
 42        lk4 = 0; // initially lock is open
 43
 44        lk5 = 0; // initially lock is open
 45
 46        lk6 = 0; // initially lock is open
 47
 48        lk7 = 0; // initially lock is open
 49
 50        lk8 = 0; // initially lock is open
 51
 52
 53    // lock phase
 54        if (p1 != 0) {
 55            lk1 = 1; // acquire lock
 56        } else {}
 57
 58        if (p2 != 0) {
 59            lk2 = 1; // acquire lock
 60        } else {}
 61
 62        if (p3 != 0) {
 63            lk3 = 1; // acquire lock
 64        } else {}
 65
 66        if (p4 != 0) {
 67            lk4 = 1; // acquire lock
 68        } else {}
 69
 70        if (p5 != 0) {
 71            lk5 = 1; // acquire lock
 72        } else {}
 73
 74        if (p6 != 0) {
 75            lk6 = 1; // acquire lock
 76        } else {}
 77
 78        if (p7 != 0) {
 79            lk7 = 1; // acquire lock
 80        } else {}
 81
 82        if (p8 != 0) {
 83            lk8 = 1; // acquire lock
 84        } else {}
 85
 86
 87    // unlock phase
 88        if (p1 != 0) {
 89            if (lk1 != 1) goto ERROR; // assertion failure
 90            lk1 = 0;
 91        } else {}
 92
 93        if (p2 != 0) {
 94            if (lk2 != 1) goto ERROR; // assertion failure
 95            lk2 = 0;
 96        } else {}
 97
 98        if (p3 != 0) {
 99            if (lk3 != 1) goto ERROR; // assertion failure
100            lk3 = 0;
101        } else {}
102
103        if (p4 != 0) {
104            if (lk4 != 1) goto ERROR; // assertion failure
105            lk4 = 0;
106        } else {}
107
108        if (p5 != 0) {
109            if (lk5 != 1) goto ERROR; // assertion failure
110            lk5 = 0;
111        } else {}
112
113        if (p6 != 0) {
114            if (lk6 != 1) goto ERROR; // assertion failure
115            lk6 = 0;
116        } else {}
117
118        if (p7 != 0) {
119            if (lk7 != 1) goto ERROR; // assertion failure
120            lk7 = 0;
121        } else {}
122
123        if (p8 != 0) {
124            if (lk8 != 1) goto ERROR; // assertion failure
125            lk8 = 0;
126        } else {}
127
128    }
129  out:
130    return 0;
131  ERROR:
132    return 0;  
133}
134
↑