Showing error 22

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_7.c
Line in file: 122
Project: SV-COMP 2012
Tools: Manual Work
Entered: 2012-11-19 13:47:39 UTC

Source: 

  1int get_exit_nondet()
  2{
  3    int retval;
  4    return (retval);
  5}
  6
  7int main()
  8{
  9    int p1;  // condition variable
 10    int lk1; // lock variable
 11
 12    int p2;  // condition variable
 13    int lk2; // lock variable
 14
 15    int p3;  // condition variable
 16    int lk3; // lock variable
 17
 18    int p4;  // condition variable
 19    int lk4; // lock variable
 20
 21    int p5;  // condition variable
 22    int lk5; // lock variable
 23
 24    int p6;  // condition variable
 25    int lk6; // lock variable
 26
 27    int p7;  // condition variable
 28    int lk7; // lock variable
 29
 30
 31    int cond;
 32
 33    while(1) {
 34        cond = get_exit_nondet();
 35        if (cond == 0) {
 36            goto out;
 37        } else {}
 38        lk1 = 0; // initially lock is open
 39
 40        lk2 = 0; // initially lock is open
 41
 42        lk3 = 0; // initially lock is open
 43
 44        lk4 = 0; // initially lock is open
 45
 46        lk5 = 0; // initially lock is open
 47
 48        lk6 = 0; // initially lock is open
 49
 50        lk7 = 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
 83    // unlock phase
 84        if (p1 != 0) {
 85            if (lk1 != 1) goto ERROR; // assertion failure
 86            lk1 = 0;
 87        } else {}
 88
 89        if (p2 != 0) {
 90            if (lk2 != 1) goto ERROR; // assertion failure
 91            lk2 = 0;
 92        } else {}
 93
 94        if (p3 != 0) {
 95            if (lk3 != 1) goto ERROR; // assertion failure
 96            lk3 = 0;
 97        } else {}
 98
 99        if (p4 != 0) {
100            if (lk4 != 1) goto ERROR; // assertion failure
101            lk4 = 0;
102        } else {}
103
104        if (p5 != 0) {
105            if (lk5 != 1) goto ERROR; // assertion failure
106            lk5 = 0;
107        } else {}
108
109        if (p6 != 0) {
110            if (lk6 != 1) goto ERROR; // assertion failure
111            lk6 = 0;
112        } else {}
113
114        if (p7 != 0) {
115            if (lk7 != 1) goto ERROR; // assertion failure
116            lk7 = 0;
117        } else {}
118
119    }
120  out:
121    return 0;
122  ERROR:
123    return 0;  
124}
125
↑