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_10.c |
Line in file: | 164 |
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 40 int cond; 41 42 while(1) { 43 cond = get_exit_nondet(); 44 if (cond == 0) { 45 goto out; 46 } else {} 47 lk1 = 0; // initially lock is open 48 49 lk2 = 0; // initially lock is open 50 51 lk3 = 0; // initially lock is open 52 53 lk4 = 0; // initially lock is open 54 55 lk5 = 0; // initially lock is open 56 57 lk6 = 0; // initially lock is open 58 59 lk7 = 0; // initially lock is open 60 61 lk8 = 0; // initially lock is open 62 63 lk9 = 0; // initially lock is open 64 65 lk10 = 0; // initially lock is open 66 67 68 // lock phase 69 if (p1 != 0) { 70 lk1 = 1; // acquire lock 71 } else {} 72 73 if (p2 != 0) { 74 lk2 = 1; // acquire lock 75 } else {} 76 77 if (p3 != 0) { 78 lk3 = 1; // acquire lock 79 } else {} 80 81 if (p4 != 0) { 82 lk4 = 1; // acquire lock 83 } else {} 84 85 if (p5 != 0) { 86 lk5 = 1; // acquire lock 87 } else {} 88 89 if (p6 != 0) { 90 lk6 = 1; // acquire lock 91 } else {} 92 93 if (p7 != 0) { 94 lk7 = 1; // acquire lock 95 } else {} 96 97 if (p8 != 0) { 98 lk8 = 1; // acquire lock 99 } else {} 100 101 if (p9 != 0) { 102 lk9 = 1; // acquire lock 103 } else {} 104 105 if (p10 != 0) { 106 lk10 = 1; // acquire lock 107 } else {} 108 109 110 // unlock phase 111 if (p1 != 0) { 112 if (lk1 != 1) goto ERROR; // assertion failure 113 lk1 = 0; 114 } else {} 115 116 if (p2 != 0) { 117 if (lk2 != 1) goto ERROR; // assertion failure 118 lk2 = 0; 119 } else {} 120 121 if (p3 != 0) { 122 if (lk3 != 1) goto ERROR; // assertion failure 123 lk3 = 0; 124 } else {} 125 126 if (p4 != 0) { 127 if (lk4 != 1) goto ERROR; // assertion failure 128 lk4 = 0; 129 } else {} 130 131 if (p5 != 0) { 132 if (lk5 != 1) goto ERROR; // assertion failure 133 lk5 = 0; 134 } else {} 135 136 if (p6 != 0) { 137 if (lk6 != 1) goto ERROR; // assertion failure 138 lk6 = 0; 139 } else {} 140 141 if (p7 != 0) { 142 if (lk7 != 1) goto ERROR; // assertion failure 143 lk7 = 0; 144 } else {} 145 146 if (p8 != 0) { 147 if (lk8 != 1) goto ERROR; // assertion failure 148 lk8 = 0; 149 } else {} 150 151 if (p9 != 0) { 152 if (lk9 != 1) goto ERROR; // assertion failure 153 lk9 = 0; 154 } else {} 155 156 if (p10 != 0) { 157 if (lk10 != 1) goto ERROR; // assertion failure 158 lk10 = 0; 159 } else {} 160 161 } 162 out: 163 return 0; 164 ERROR: 165 return 0; 166} 167