// c::worker_1 // file pgsql_two.c line 42 void * worker_1(void *); // c::worker_2 // file pgsql_two.c line 61 void * worker_2(void *); // c::main // file pgsql_two.c line 94 int _main(void); // c::__CPROVER_initialize // file line 14 void __CPROVER_initialize(void); #include #include // c::worker_1$tmp_guard0 // _Bool tmp_guard; // c::worker_1$tmp_guard1 // _Bool tmp_guard1; // c::worker_1$tmp_guard2 // _Bool tmp_guard2; // c::worker_2$tmp_guard0 // _Bool tmp_guard3; // c::worker_2$tmp_guard1 // _Bool tmp_guard4; // c::worker_2$tmp_guard2 // _Bool tmp_guard5; // c::latch1 // file pgsql_two.c line 6 _Bool latch1; // c::flag1 // file pgsql_two.c line 7 _Bool flag1; // c::latch2 // file pgsql_two.c line 8 _Bool latch2; // c::flag2 // file pgsql_two.c line 8 _Bool flag2; // c::__unbuffered_tmp2 // file pgsql_two.c line 14 _Bool __unbuffered_tmp2; // main // int main(void) { __CPROVER_initialize(); _main(); } // c::worker_1 // file pgsql_two.c line 42 void * worker_1(void * arg) { // file pgsql_two.c line 47 function worker_1 L1: // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file pgsql_two.c line 47 function worker_1 tmp_guard=(!(!latch1)); // file pgsql_two.c line 47 function worker_1 // ATOMIC_END __CPROVER_atomic_end(); // file pgsql_two.c line 47 function worker_1 if( tmp_guard ) goto L2; // file pgsql_two.c line 47 function worker_1 goto L1; // file pgsql_two.c line 48 function worker_1 L2: // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file pgsql_two.c line 48 function worker_1 tmp_guard1=((!latch1) || flag1); // file pgsql_two.c line 48 function worker_1 // ATOMIC_END __CPROVER_atomic_end(); // file pgsql_two.c line 48 function worker_1 assert(tmp_guard1); // file pgsql_two.c line 49 function worker_1 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file pgsql_two.c line 49 function worker_1 latch1=(_Bool)(0); // file pgsql_two.c line 49 function worker_1 // ATOMIC_END __CPROVER_atomic_end(); // file pgsql_two.c line 50 function worker_1 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file pgsql_two.c line 50 function worker_1 tmp_guard2=(!flag1); // file pgsql_two.c line 50 function worker_1 // ATOMIC_END __CPROVER_atomic_end(); // file pgsql_two.c line 50 function worker_1 if( tmp_guard2 ) goto L3; // file pgsql_two.c line 52 function worker_1 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file pgsql_two.c line 52 function worker_1 flag1=(_Bool)(0); // file pgsql_two.c line 52 function worker_1 // ATOMIC_END __CPROVER_atomic_end(); // file pgsql_two.c line 53 function worker_1 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file pgsql_two.c line 53 function worker_1 flag2=(_Bool)(1); // file pgsql_two.c line 53 function worker_1 // ATOMIC_END __CPROVER_atomic_end(); // file pgsql_two.c line 54 function worker_1 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file pgsql_two.c line 54 function worker_1 latch2=(_Bool)(1); // file pgsql_two.c line 54 function worker_1 // ATOMIC_END __CPROVER_atomic_end(); // file pgsql_two.c line 45 function worker_1 L3: goto L1; // file pgsql_two.c line 59 function worker_1 return nondet_ptr(); // file pgsql_two.c line 59 function worker_1 } // c::worker_2 // file pgsql_two.c line 61 void * worker_2(void * arg1) { // file pgsql_two.c line 66 function worker_2 L1: // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file pgsql_two.c line 66 function worker_2 tmp_guard3=(!(!latch2)); // file pgsql_two.c line 66 function worker_2 // ATOMIC_END __CPROVER_atomic_end(); // file pgsql_two.c line 66 function worker_2 if( tmp_guard3 ) goto L2; // file pgsql_two.c line 66 function worker_2 goto L1; // file pgsql_two.c line 67 function worker_2 L2: // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file pgsql_two.c line 67 function worker_2 tmp_guard4=((!latch2) || flag2); // file pgsql_two.c line 67 function worker_2 // ATOMIC_END __CPROVER_atomic_end(); // file pgsql_two.c line 67 function worker_2 assert(tmp_guard4); // file pgsql_two.c line 68 function worker_2 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file pgsql_two.c line 68 function worker_2 latch2=(_Bool)(0); // file pgsql_two.c line 68 function worker_2 // ATOMIC_END __CPROVER_atomic_end(); // file pgsql_two.c line 71 function worker_2 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file pgsql_two.c line 71 function worker_2 tmp_guard5=(!flag2); // file pgsql_two.c line 71 function worker_2 // ATOMIC_END __CPROVER_atomic_end(); // file pgsql_two.c line 71 function worker_2 if( tmp_guard5 ) goto L3; // file pgsql_two.c line 73 function worker_2 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file pgsql_two.c line 73 function worker_2 flag2=(_Bool)(0); // file pgsql_two.c line 73 function worker_2 // ATOMIC_END __CPROVER_atomic_end(); // file pgsql_two.c line 74 function worker_2 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file pgsql_two.c line 74 function worker_2 flag1=(_Bool)(1); // file pgsql_two.c line 74 function worker_2 // ATOMIC_END __CPROVER_atomic_end(); // file pgsql_two.c line 76 function worker_2 // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file pgsql_two.c line 76 function worker_2 latch1=(_Bool)(1); // file pgsql_two.c line 76 function worker_2 // ATOMIC_END __CPROVER_atomic_end(); // file pgsql_two.c line 64 function worker_2 L3: goto L1; // file pgsql_two.c line 81 function worker_2 return nondet_ptr(); // file pgsql_two.c line 81 function worker_2 } // c::main // file pgsql_two.c line 94 int _main(void) { pthread_t __pt0; pthread_t __pt1; // file pgsql_two.c line 98 function main // START_THREAD pthread_create(&__pt0, 0, worker_1, 0); // file pgsql_two.c line 99 function main L1: // START_THREAD pthread_create(&__pt1, 0, worker_2, 0); // file pgsql_two.c line 106 function main L2: return 0; // file pgsql_two.c line 107 function main } // c::__CPROVER_initialize // file line 14 void __CPROVER_initialize(void) { // file line 26 // file line 27 // file line 28 // file line 29 // file line 38 // file pgsql_two.c line 6 latch1=(_Bool)(1); // file pgsql_two.c line 7 flag1=(_Bool)(1); // file pgsql_two.c line 8 latch2=false; // file pgsql_two.c line 8 flag2=false; // file pgsql_two.c line 14 __unbuffered_tmp2=false; }