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_13.c |
Line in file: | 206 |
Project: | SV-COMP 2012 |
Tools: |
Manual Work
|
Entered: | 2012-11-19 13:47:39 UTC |
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 int p8; // condition variable 31 int lk8; // lock variable 32 33 int p9; // condition variable 34 int lk9; // lock variable 35 36 int p10; // condition variable 37 int lk10; // lock variable 38 39 int p11; // condition variable 40 int lk11; // lock variable 41 42 int p12; // condition variable 43 int lk12; // lock variable 44 45 int p13; // condition variable 46 int lk13; // lock variable 47 48 49 int cond; 50 51 while(1) { 52 cond = get_exit_nondet(); 53 if (cond == 0) { 54 goto out; 55 } else {} 56 lk1 = 0; // initially lock is open 57 58 lk2 = 0; // initially lock is open 59 60 lk3 = 0; // initially lock is open 61 62 lk4 = 0; // initially lock is open 63 64 lk5 = 0; // initially lock is open 65 66 lk6 = 0; // initially lock is open 67 68 lk7 = 0; // initially lock is open 69 70 lk8 = 0; // initially lock is open 71 72 lk9 = 0; // initially lock is open 73 74 lk10 = 0; // initially lock is open 75 76 lk11 = 0; // initially lock is open 77 78 lk12 = 0; // initially lock is open 79 80 lk13 = 0; // initially lock is open 81 82 83 // lock phase 84 if (p1 != 0) { 85 lk1 = 1; // acquire lock 86 } else {} 87 88 if (p2 != 0) { 89 lk2 = 1; // acquire lock 90 } else {} 91 92 if (p3 != 0) { 93 lk3 = 1; // acquire lock 94 } else {} 95 96 if (p4 != 0) { 97 lk4 = 1; // acquire lock 98 } else {} 99 100 if (p5 != 0) { 101 lk5 = 1; // acquire lock 102 } else {} 103 104 if (p6 != 0) { 105 lk6 = 1; // acquire lock 106 } else {} 107 108 if (p7 != 0) { 109 lk7 = 1; // acquire lock 110 } else {} 111 112 if (p8 != 0) { 113 lk8 = 1; // acquire lock 114 } else {} 115 116 if (p9 != 0) { 117 lk9 = 1; // acquire lock 118 } else {} 119 120 if (p10 != 0) { 121 lk10 = 1; // acquire lock 122 } else {} 123 124 if (p11 != 0) { 125 lk11 = 1; // acquire lock 126 } else {} 127 128 if (p12 != 0) { 129 lk12 = 1; // acquire lock 130 } else {} 131 132 if (p13 != 0) { 133 lk13 = 1; // acquire lock 134 } else {} 135 136 137 // unlock phase 138 if (p1 != 0) { 139 if (lk1 != 1) goto ERROR; // assertion failure 140 lk1 = 0; 141 } else {} 142 143 if (p2 != 0) { 144 if (lk2 != 1) goto ERROR; // assertion failure 145 lk2 = 0; 146 } else {} 147 148 if (p3 != 0) { 149 if (lk3 != 1) goto ERROR; // assertion failure 150 lk3 = 0; 151 } else {} 152 153 if (p4 != 0) { 154 if (lk4 != 1) goto ERROR; // assertion failure 155 lk4 = 0; 156 } else {} 157 158 if (p5 != 0) { 159 if (lk5 != 1) goto ERROR; // assertion failure 160 lk5 = 0; 161 } else {} 162 163 if (p6 != 0) { 164 if (lk6 != 1) goto ERROR; // assertion failure 165 lk6 = 0; 166 } else {} 167 168 if (p7 != 0) { 169 if (lk7 != 1) goto ERROR; // assertion failure 170 lk7 = 0; 171 } else {} 172 173 if (p8 != 0) { 174 if (lk8 != 1) goto ERROR; // assertion failure 175 lk8 = 0; 176 } else {} 177 178 if (p9 != 0) { 179 if (lk9 != 1) goto ERROR; // assertion failure 180 lk9 = 0; 181 } else {} 182 183 if (p10 != 0) { 184 if (lk10 != 1) goto ERROR; // assertion failure 185 lk10 = 0; 186 } else {} 187 188 if (p11 != 0) { 189 if (lk11 != 1) goto ERROR; // assertion failure 190 lk11 = 0; 191 } else {} 192 193 if (p12 != 0) { 194 if (lk12 != 1) goto ERROR; // assertion failure 195 lk12 = 0; 196 } else {} 197 198 if (p13 != 0) { 199 if (lk13 != 1) goto ERROR; // assertion failure 200 lk13 = 0; 201 } else {} 202 203 } 204 out: 205 return 0; 206 ERROR: 207 return 0; 208} 209