/* TAGS: c big */ /* VERIFY_OPTS: -o nofail:malloc */ // Source: Azadeh Farzan, Zachary Kincaid, Andreas Podelski: "Inductive Data // Flow Graphs", POPL 2013 #include extern void __VERIFIER_error(void); extern void __VERIFIER_assume(int); void __VERIFIER_assert(int cond) { if (!(cond)) { ERROR: __VERIFIER_error(); /* ERROR */ } return; } extern void __VERIFIER_atomic_begin(); extern void __VERIFIER_atomic_end(); volatile int x; #define N 50 void* thr1(void* arg) { __VERIFIER_assert(x < N); } void* thr2(void* arg) { int t; t = x; x = t + 1; } int main(int argc, char* argv[]) { pthread_t t1, t2; int i; x = 0; pthread_create(&t1, 0, thr1, 0); for (i = 0; i < N; i++) { pthread_create(&t2, 0, thr2, 0); } return 0; }