// c::BlockOnIdle // file sober-fixed.c line 31 void * BlockOnIdle(void *); // c::NotifyPotentialWork // file sober-fixed.c line 45 void * NotifyPotentialWork(void *); // c::main // file sober-fixed.c line 58 int _main(void); // c::__CPROVER_initialize // file line 14 void __CPROVER_initialize(void); #include #include // c::__unbuffered_prod_done // file sober-fixed.c line 42 _Bool __unbuffered_prod_done; // c::BlockOnIdle$tmp_guard0 // _Bool tmp_guard; // c::BlockOnIdle$tmp_guard1 // _Bool tmp_guard1; // c::BlockOnIdle$tmp_guard2 // _Bool tmp_guard2; // c::BlockOnIdle$tmp_guard3 // _Bool tmp_guard3; // c::BlockOnIdle$tmp_guard4 // _Bool tmp_guard4; // c::NotifyPotentialWork$tmp_guard0 // _Bool tmp_guard5; // c::NotifyPotentialWork$tmp_guard1 // _Bool tmp_guard6; // c::NotifyPotentialWork$tmp_guard2 // _Bool tmp_guard7; // c::main$tmp_guard0 // _Bool tmp_guard8; // c::isIdling // file sober-fixed.c line 1 _Bool isIdling; // c::hasWork // file sober-fixed.c line 2 _Bool hasWork; // c::__unbuffered_condVariable // file sober-fixed.c line 3 int __unbuffered_condVariable; // main // int main(void) { __CPROVER_initialize(); _main(); } // c::BlockOnIdle // file sober-fixed.c line 31 void * BlockOnIdle(void * arg) { // file sober-fixed.c line 33 function BlockOnIdle // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober-fixed.c line 33 function BlockOnIdle // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober-fixed.c line 33 function BlockOnIdle tmp_guard=((__unbuffered_condVariable==0) || (__unbuffered_condVariable==2)); // file sober-fixed.c line 33 function BlockOnIdle // ATOMIC_END __CPROVER_atomic_end(); // file sober-fixed.c line 33 function BlockOnIdle __CPROVER_assume(tmp_guard); // file sober-fixed.c line 33 function BlockOnIdle // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober-fixed.c line 33 function BlockOnIdle __unbuffered_condVariable=((__unbuffered_condVariable+1)); // file sober-fixed.c line 33 function BlockOnIdle // ATOMIC_END __CPROVER_atomic_end(); // file sober-fixed.c line 33 function BlockOnIdle // file sober-fixed.c line 33 function BlockOnIdle // ATOMIC_END __CPROVER_atomic_end(); // file sober-fixed.c line 34 function BlockOnIdle // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober-fixed.c line 34 function BlockOnIdle isIdling=(_Bool)(1); // file sober-fixed.c line 34 function BlockOnIdle // ATOMIC_END __CPROVER_atomic_end(); // file sober-fixed.c line 35 function BlockOnIdle // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober-fixed.c line 35 function BlockOnIdle // ATOMIC_END __CPROVER_atomic_end(); // file sober-fixed.c line 36 function BlockOnIdle // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober-fixed.c line 36 function BlockOnIdle tmp_guard1=(!(!hasWork)); // file sober-fixed.c line 36 function BlockOnIdle // ATOMIC_END __CPROVER_atomic_end(); // file sober-fixed.c line 36 function BlockOnIdle if( tmp_guard1 ) goto L1; // file sober-fixed.c line 37 function BlockOnIdle // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober-fixed.c line 37 function BlockOnIdle // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober-fixed.c line 37 function BlockOnIdle tmp_guard2=(__unbuffered_condVariable==1); // file sober-fixed.c line 37 function BlockOnIdle // ATOMIC_END __CPROVER_atomic_end(); // file sober-fixed.c line 37 function BlockOnIdle __CPROVER_assume(tmp_guard2); // file sober-fixed.c line 37 function BlockOnIdle // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober-fixed.c line 37 function BlockOnIdle __unbuffered_condVariable=2; // file sober-fixed.c line 37 function BlockOnIdle // ATOMIC_END __CPROVER_atomic_end(); // file sober-fixed.c line 37 function BlockOnIdle // ATOMIC_END __CPROVER_atomic_end(); // file sober-fixed.c line 37 function BlockOnIdle // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober-fixed.c line 37 function BlockOnIdle tmp_guard3=(__unbuffered_condVariable==4); // file sober-fixed.c line 37 function BlockOnIdle // ATOMIC_END __CPROVER_atomic_end(); // file sober-fixed.c line 37 function BlockOnIdle __CPROVER_assume(tmp_guard3); // file sober-fixed.c line 37 function BlockOnIdle // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober-fixed.c line 37 function BlockOnIdle tmp_guard4=(__unbuffered_condVariable==0); // file sober-fixed.c line 37 function BlockOnIdle // ATOMIC_END __CPROVER_atomic_end(); // file sober-fixed.c line 37 function BlockOnIdle __CPROVER_assume(tmp_guard4); // file sober-fixed.c line 37 function BlockOnIdle // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober-fixed.c line 37 function BlockOnIdle __unbuffered_condVariable=1; // file sober-fixed.c line 37 function BlockOnIdle // ATOMIC_END __CPROVER_atomic_end(); // file sober-fixed.c line 38 function BlockOnIdle L1: // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober-fixed.c line 38 function BlockOnIdle isIdling=(_Bool)(0); // file sober-fixed.c line 38 function BlockOnIdle // ATOMIC_END __CPROVER_atomic_end(); // file sober-fixed.c line 39 function BlockOnIdle // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober-fixed.c line 39 function BlockOnIdle __unbuffered_condVariable=0; // file sober-fixed.c line 39 function BlockOnIdle // ATOMIC_END __CPROVER_atomic_end(); // file sober-fixed.c line 40 function BlockOnIdle return nondet_ptr(); // file sober-fixed.c line 40 function BlockOnIdle } // c::NotifyPotentialWork // file sober-fixed.c line 45 void * NotifyPotentialWork(void * arg1) { // file sober-fixed.c line 47 function NotifyPotentialWork // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober-fixed.c line 47 function NotifyPotentialWork hasWork=(_Bool)(1); // file sober-fixed.c line 47 function NotifyPotentialWork // ATOMIC_END __CPROVER_atomic_end(); // file sober-fixed.c line 48 function NotifyPotentialWork // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober-fixed.c line 48 function NotifyPotentialWork // ATOMIC_END __CPROVER_atomic_end(); // file sober-fixed.c line 49 function NotifyPotentialWork // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober-fixed.c line 49 function NotifyPotentialWork tmp_guard5=(!isIdling); // file sober-fixed.c line 49 function NotifyPotentialWork // ATOMIC_END __CPROVER_atomic_end(); // file sober-fixed.c line 49 function NotifyPotentialWork if( tmp_guard5 ) goto L1; // file sober-fixed.c line 51 function NotifyPotentialWork // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober-fixed.c line 51 function NotifyPotentialWork // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober-fixed.c line 51 function NotifyPotentialWork tmp_guard6=((__unbuffered_condVariable==0) || (__unbuffered_condVariable==2)); // file sober-fixed.c line 51 function NotifyPotentialWork // ATOMIC_END __CPROVER_atomic_end(); // file sober-fixed.c line 51 function NotifyPotentialWork __CPROVER_assume(tmp_guard6); // file sober-fixed.c line 51 function NotifyPotentialWork // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober-fixed.c line 51 function NotifyPotentialWork __unbuffered_condVariable=((__unbuffered_condVariable+1)); // file sober-fixed.c line 51 function NotifyPotentialWork // ATOMIC_END __CPROVER_atomic_end(); // file sober-fixed.c line 51 function NotifyPotentialWork // file sober-fixed.c line 51 function NotifyPotentialWork // ATOMIC_END __CPROVER_atomic_end(); // file sober-fixed.c line 52 function NotifyPotentialWork // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober-fixed.c line 52 function NotifyPotentialWork tmp_guard7=(__unbuffered_condVariable==2); // file sober-fixed.c line 52 function NotifyPotentialWork // ATOMIC_END __CPROVER_atomic_end(); // file sober-fixed.c line 52 function NotifyPotentialWork __CPROVER_assume(tmp_guard7); // file sober-fixed.c line 52 function NotifyPotentialWork // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober-fixed.c line 52 function NotifyPotentialWork __unbuffered_condVariable=4; // file sober-fixed.c line 52 function NotifyPotentialWork // ATOMIC_END __CPROVER_atomic_end(); // file sober-fixed.c line 53 function NotifyPotentialWork // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober-fixed.c line 53 function NotifyPotentialWork __unbuffered_condVariable=0; // file sober-fixed.c line 53 function NotifyPotentialWork // ATOMIC_END __CPROVER_atomic_end(); // file sober-fixed.c line 55 function NotifyPotentialWork L1: // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober-fixed.c line 55 function NotifyPotentialWork __unbuffered_prod_done=(_Bool)(1); // file sober-fixed.c line 55 function NotifyPotentialWork // ATOMIC_END __CPROVER_atomic_end(); // file sober-fixed.c line 56 function NotifyPotentialWork return nondet_ptr(); // file sober-fixed.c line 56 function NotifyPotentialWork } // c::main // file sober-fixed.c line 58 int _main(void) { pthread_t __pt0; pthread_t __pt1; // file sober-fixed.c line 60 function main // START_THREAD pthread_create(&__pt0, 0, BlockOnIdle, 0); // file sober-fixed.c line 61 function main L1: // START_THREAD pthread_create(&__pt1, 0, NotifyPotentialWork, 0); // file sober-fixed.c line 62 function main L2: // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober-fixed.c line 62 function main tmp_guard8=((!__unbuffered_prod_done) || (__unbuffered_condVariable!=2)); // file sober-fixed.c line 62 function main // ATOMIC_END __CPROVER_atomic_end(); // file sober-fixed.c line 62 function main assert(tmp_guard8); // file sober-fixed.c line 63 function main return nondet_int(); // file sober-fixed.c line 63 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 sober-fixed.c line 1 isIdling=(_Bool)(0); // file sober-fixed.c line 2 hasWork=(_Bool)(0); // file sober-fixed.c line 3 __unbuffered_condVariable=0; // file sober-fixed.c line 42 __unbuffered_prod_done=(_Bool)(0); }