source:
CIVL/examples/pthread/cprover/45_monabsex1_vs_true.c@
8ed2d3b
| Last change on this file since 8ed2d3b was e3151da, checked in by , 12 years ago | |
|---|---|
|
|
| File size: 309 bytes | |
| Line | |
|---|---|
| 1 | #include <pthread.h> |
| 2 | |
| 3 | #define assert(e) { if(!(e)) { ERROR: goto ERROR; (void)0; } } |
| 4 | |
| 5 | int s; |
| 6 | |
| 7 | void* thr1(void* arg) |
| 8 | { |
| 9 | int l = __VERIFIER_nondet_int(); |
| 10 | l = 4; |
| 11 | s = l; |
| 12 | assert(s == l); |
| 13 | |
| 14 | return 0; |
| 15 | } |
| 16 | |
| 17 | int main() |
| 18 | { |
| 19 | s = __VERIFIER_nondet_int(); |
| 20 | |
| 21 | pthread_t t; |
| 22 | |
| 23 | while(1) pthread_create(&t, 0, thr1, 0); |
| 24 | } |
| 25 |
Note:
See TracBrowser
for help on using the repository browser.
