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_5.c |
Line in file: | 94 |
Project: | SV-COMP 2012 |
Tools: |
Manual Work
|
Entered: | 2012-11-19 13:47:39 UTC |
64 65 // unlock phase 66 if (p1 != 0) { 67 if (lk1 != 1) goto ERROR; // assertion failure 68 lk1 = 0; 69 } else {} 70 71 if (p2 != 0) { 72 if (lk2 != 1) goto ERROR; // assertion failure 73 lk2 = 0; 74 } else {} 75 76 if (p3 != 0) { 77 if (lk3 != 1) goto ERROR; // assertion failure 78 lk3 = 0; 79 } else {} 80 81 if (p4 != 0) { 82 if (lk4 != 1) goto ERROR; // assertion failure 83 lk4 = 0; 84 } else {} 85 86 if (p5 != 0) { 87 if (lk5 != 1) goto ERROR; // assertion failure 88 lk5 = 0; 89 } else {} 90 91 } 92 out: 93 return 0; 94 ERROR: 95 return 0; 96} 97