// c::BlockOnIdle // file sober.c line 31 void * BlockOnIdle(void *); // c::NotifyPotentialWork // file sober.c line 44 void * NotifyPotentialWork(void *); // c::main // file sober.c line 56 int _main(void); // c::__CPROVER_initialize // file line 14 void __CPROVER_initialize(void); #include #include // 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$w_buff0 // _Bool cisIdlingw_buff0; // c::isIdling$w_buff1 // _Bool cisIdlingw_buff1; // c::isIdling$w_buff0_used // _Bool cisIdlingw_buff0_used; // c::isIdling$w_buff1_used // _Bool cisIdlingw_buff1_used; // c::isIdling$mem_tmp // _Bool cisIdlingmem_tmp; // c::isIdling$flush_delayed // _Bool cisIdlingflush_delayed; // c::isIdling$read_delayed // _Bool cisIdlingread_delayed; // c::isIdling$read_delayed_var // _Bool * cisIdlingread_delayed_var; // c::isIdling$r_buff0_thd0 // _Bool cisIdlingr_buff0_thd0; // c::isIdling$r_buff1_thd0 // _Bool cisIdlingr_buff1_thd0; // c::isIdling$r_buff0_thd1 // _Bool cisIdlingr_buff0_thd1; // c::isIdling$r_buff1_thd1 // _Bool cisIdlingr_buff1_thd1; // c::isIdling$r_buff0_thd2 // _Bool cisIdlingr_buff0_thd2; // c::isIdling$r_buff1_thd2 // _Bool cisIdlingr_buff1_thd2; // weak::choice0 // _Bool weakchoice0; // weak::choice2 // _Bool weakchoice2; // c::isIdling // file sober.c line 1 _Bool isIdling; // c::hasWork // file sober.c line 2 _Bool hasWork; // c::__unbuffered_condVariable // file sober.c line 3 int __unbuffered_condVariable; // c::__unbuffered_prod_done // file sober.c line 41 _Bool __unbuffered_prod_done; // main // int main(void) { cisIdlingw_buff0_used=false; cisIdlingw_buff1_used=false; cisIdlingflush_delayed=false; cisIdlingread_delayed=false; cisIdlingread_delayed_var=0; cisIdlingr_buff0_thd0=false; cisIdlingr_buff0_thd1=false; cisIdlingr_buff0_thd2=false; cisIdlingr_buff1_thd0=false; cisIdlingr_buff1_thd1=false; cisIdlingr_buff1_thd2=false; __CPROVER_initialize(); _main(); } // c::BlockOnIdle // file sober.c line 31 void * BlockOnIdle(void * arg) { // file sober.c line 33 function BlockOnIdle // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober.c line 33 function BlockOnIdle // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober.c line 33 function BlockOnIdle tmp_guard=((__unbuffered_condVariable==0) || (__unbuffered_condVariable==2)); // file sober.c line 33 function BlockOnIdle // ATOMIC_END __CPROVER_atomic_end(); // file sober.c line 33 function BlockOnIdle __CPROVER_assume(tmp_guard); // file sober.c line 33 function BlockOnIdle // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober.c line 33 function BlockOnIdle __unbuffered_condVariable=((__unbuffered_condVariable+1)); // file sober.c line 33 function BlockOnIdle // ATOMIC_END __CPROVER_atomic_end(); // file sober.c line 33 function BlockOnIdle // file sober.c line 33 function BlockOnIdle // ATOMIC_END __CPROVER_atomic_end(); // file sober.c line 34 function BlockOnIdle // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober.c line 34 function BlockOnIdle cisIdlingw_buff1=cisIdlingw_buff0; // file sober.c line 34 function BlockOnIdle cisIdlingw_buff0=(_Bool)(1); // file sober.c line 34 function BlockOnIdle cisIdlingw_buff1_used=cisIdlingw_buff0_used; // file sober.c line 34 function BlockOnIdle cisIdlingw_buff0_used=true; // file sober.c line 34 function BlockOnIdle assert((!(cisIdlingw_buff1_used && cisIdlingw_buff0_used))); // file sober.c line 34 function BlockOnIdle cisIdlingr_buff1_thd0=cisIdlingr_buff0_thd0; // file sober.c line 34 function BlockOnIdle cisIdlingr_buff1_thd1=cisIdlingr_buff0_thd1; // file sober.c line 34 function BlockOnIdle cisIdlingr_buff1_thd2=cisIdlingr_buff0_thd2; // file sober.c line 34 function BlockOnIdle cisIdlingr_buff0_thd1=true; // file sober.c line 34 function BlockOnIdle // ATOMIC_END __CPROVER_atomic_end(); // file sober.c line 35 function BlockOnIdle // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober.c line 35 function BlockOnIdle tmp_guard1=(!(!hasWork)); // file sober.c line 35 function BlockOnIdle // ATOMIC_END __CPROVER_atomic_end(); // file sober.c line 35 function BlockOnIdle if( tmp_guard1 ) goto L1; // file sober.c line 36 function BlockOnIdle // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober.c line 36 function BlockOnIdle // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober.c line 36 function BlockOnIdle tmp_guard2=(__unbuffered_condVariable==1); // file sober.c line 36 function BlockOnIdle // ATOMIC_END __CPROVER_atomic_end(); // file sober.c line 36 function BlockOnIdle __CPROVER_assume(tmp_guard2); // file sober.c line 36 function BlockOnIdle // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober.c line 36 function BlockOnIdle __unbuffered_condVariable=2; // file sober.c line 36 function BlockOnIdle // ATOMIC_END __CPROVER_atomic_end(); // file sober.c line 36 function BlockOnIdle // ATOMIC_END __CPROVER_atomic_end(); // file sober.c line 36 function BlockOnIdle // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober.c line 36 function BlockOnIdle tmp_guard3=(__unbuffered_condVariable==4); // file sober.c line 36 function BlockOnIdle // ATOMIC_END __CPROVER_atomic_end(); // file sober.c line 36 function BlockOnIdle __CPROVER_assume(tmp_guard3); // file sober.c line 36 function BlockOnIdle // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober.c line 36 function BlockOnIdle tmp_guard4=(__unbuffered_condVariable==0); // file sober.c line 36 function BlockOnIdle // ATOMIC_END __CPROVER_atomic_end(); // file sober.c line 36 function BlockOnIdle __CPROVER_assume(tmp_guard4); // file sober.c line 36 function BlockOnIdle // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober.c line 36 function BlockOnIdle __unbuffered_condVariable=1; // file sober.c line 36 function BlockOnIdle // ATOMIC_END __CPROVER_atomic_end(); // file sober.c line 37 function BlockOnIdle L1: // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober.c line 37 function BlockOnIdle isIdling=(_Bool)(0); // file sober.c line 37 function BlockOnIdle // ATOMIC_END __CPROVER_atomic_end(); // file sober.c line 38 function BlockOnIdle // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober.c line 38 function BlockOnIdle __unbuffered_condVariable=0; // file sober.c line 38 function BlockOnIdle // ATOMIC_END __CPROVER_atomic_end(); // file sober.c line 39 function BlockOnIdle return nondet_ptr(); // file sober.c line 39 function BlockOnIdle } // c::NotifyPotentialWork // file sober.c line 44 void * NotifyPotentialWork(void * arg1) { // file sober.c line 46 function NotifyPotentialWork // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober.c line 46 function NotifyPotentialWork hasWork=(_Bool)(1); // file sober.c line 46 function NotifyPotentialWork // ATOMIC_END __CPROVER_atomic_end(); // file sober.c line 47 function NotifyPotentialWork // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober.c line 47 function NotifyPotentialWork weakchoice0=nondet_bool(); // file sober.c line 47 function NotifyPotentialWork weakchoice2=nondet_bool(); // file sober.c line 47 function NotifyPotentialWork cisIdlingflush_delayed=weakchoice2; // file sober.c line 47 function NotifyPotentialWork cisIdlingmem_tmp=isIdling; // file sober.c line 47 function NotifyPotentialWork isIdling=(((!cisIdlingw_buff0_used) || (((!cisIdlingr_buff0_thd2) && (!cisIdlingw_buff1_used)) || ((!cisIdlingr_buff0_thd2) && (!cisIdlingr_buff1_thd2))))? isIdling:((cisIdlingw_buff0_used && cisIdlingr_buff0_thd2)? cisIdlingw_buff0:cisIdlingw_buff1)); // file sober.c line 47 function NotifyPotentialWork cisIdlingw_buff0=(weakchoice2? cisIdlingw_buff0:(((!cisIdlingw_buff0_used) || (((!cisIdlingr_buff0_thd2) && (!cisIdlingw_buff1_used)) || ((!cisIdlingr_buff0_thd2) && (!cisIdlingr_buff1_thd2))))? cisIdlingw_buff0:((cisIdlingw_buff0_used && cisIdlingr_buff0_thd2)? cisIdlingw_buff0:cisIdlingw_buff0))); // file sober.c line 47 function NotifyPotentialWork cisIdlingw_buff1=(weakchoice2? cisIdlingw_buff1:(((!cisIdlingw_buff0_used) || (((!cisIdlingr_buff0_thd2) && (!cisIdlingw_buff1_used)) || ((!cisIdlingr_buff0_thd2) && (!cisIdlingr_buff1_thd2))))? cisIdlingw_buff1:((cisIdlingw_buff0_used && cisIdlingr_buff0_thd2)? cisIdlingw_buff1:cisIdlingw_buff1))); // file sober.c line 47 function NotifyPotentialWork cisIdlingw_buff0_used=(weakchoice2? cisIdlingw_buff0_used:(((!cisIdlingw_buff0_used) || (((!cisIdlingr_buff0_thd2) && (!cisIdlingw_buff1_used)) || ((!cisIdlingr_buff0_thd2) && (!cisIdlingr_buff1_thd2))))? cisIdlingw_buff0_used:((cisIdlingw_buff0_used && cisIdlingr_buff0_thd2)? false:cisIdlingw_buff0_used))); // file sober.c line 47 function NotifyPotentialWork cisIdlingw_buff1_used=(weakchoice2? cisIdlingw_buff1_used:(((!cisIdlingw_buff0_used) || (((!cisIdlingr_buff0_thd2) && (!cisIdlingw_buff1_used)) || ((!cisIdlingr_buff0_thd2) && (!cisIdlingr_buff1_thd2))))? cisIdlingw_buff1_used:((cisIdlingw_buff0_used && cisIdlingr_buff0_thd2)? false:false))); // file sober.c line 47 function NotifyPotentialWork cisIdlingr_buff0_thd2=(weakchoice2? cisIdlingr_buff0_thd2:(((!cisIdlingw_buff0_used) || (((!cisIdlingr_buff0_thd2) && (!cisIdlingw_buff1_used)) || ((!cisIdlingr_buff0_thd2) && (!cisIdlingr_buff1_thd2))))? cisIdlingr_buff0_thd2:((cisIdlingw_buff0_used && cisIdlingr_buff0_thd2)? false:cisIdlingr_buff0_thd2))); // file sober.c line 47 function NotifyPotentialWork cisIdlingr_buff1_thd2=(weakchoice2? cisIdlingr_buff1_thd2:(((!cisIdlingw_buff0_used) || (((!cisIdlingr_buff0_thd2) && (!cisIdlingw_buff1_used)) || ((!cisIdlingr_buff0_thd2) && (!cisIdlingr_buff1_thd2))))? cisIdlingr_buff1_thd2:((cisIdlingw_buff0_used && cisIdlingr_buff0_thd2)? false:false))); // file sober.c line 47 function NotifyPotentialWork tmp_guard5=(!isIdling); // file sober.c line 47 function NotifyPotentialWork isIdling=(cisIdlingflush_delayed? cisIdlingmem_tmp:isIdling); // file sober.c line 47 function NotifyPotentialWork cisIdlingflush_delayed=false; // file sober.c line 47 function NotifyPotentialWork // ATOMIC_END __CPROVER_atomic_end(); // file sober.c line 47 function NotifyPotentialWork if( tmp_guard5 ) goto L1; // file sober.c line 49 function NotifyPotentialWork // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober.c line 49 function NotifyPotentialWork // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober.c line 49 function NotifyPotentialWork tmp_guard6=((__unbuffered_condVariable==0) || (__unbuffered_condVariable==2)); // file sober.c line 49 function NotifyPotentialWork // ATOMIC_END __CPROVER_atomic_end(); // file sober.c line 49 function NotifyPotentialWork __CPROVER_assume(tmp_guard6); // file sober.c line 49 function NotifyPotentialWork // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober.c line 49 function NotifyPotentialWork __unbuffered_condVariable=((__unbuffered_condVariable+1)); // file sober.c line 49 function NotifyPotentialWork // ATOMIC_END __CPROVER_atomic_end(); // file sober.c line 49 function NotifyPotentialWork // file sober.c line 49 function NotifyPotentialWork // ATOMIC_END __CPROVER_atomic_end(); // file sober.c line 50 function NotifyPotentialWork // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober.c line 50 function NotifyPotentialWork tmp_guard7=(__unbuffered_condVariable==2); // file sober.c line 50 function NotifyPotentialWork // ATOMIC_END __CPROVER_atomic_end(); // file sober.c line 50 function NotifyPotentialWork __CPROVER_assume(tmp_guard7); // file sober.c line 50 function NotifyPotentialWork // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober.c line 50 function NotifyPotentialWork __unbuffered_condVariable=4; // file sober.c line 50 function NotifyPotentialWork // ATOMIC_END __CPROVER_atomic_end(); // file sober.c line 51 function NotifyPotentialWork // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober.c line 51 function NotifyPotentialWork __unbuffered_condVariable=0; // file sober.c line 51 function NotifyPotentialWork // ATOMIC_END __CPROVER_atomic_end(); // file sober.c line 53 function NotifyPotentialWork L1: // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober.c line 53 function NotifyPotentialWork __unbuffered_prod_done=(_Bool)(1); // file sober.c line 53 function NotifyPotentialWork // ATOMIC_END __CPROVER_atomic_end(); // file sober.c line 54 function NotifyPotentialWork return nondet_ptr(); // file sober.c line 54 function NotifyPotentialWork } // c::main // file sober.c line 56 int _main(void) { pthread_t __pt0; pthread_t __pt1; // file sober.c line 58 function main // START_THREAD pthread_create(&__pt0, 0, BlockOnIdle, 0); // file sober.c line 59 function main L1: // START_THREAD pthread_create(&__pt1, 0, NotifyPotentialWork, 0); // file sober.c line 60 function main L2: // ATOMIC_BEGIN __CPROVER_atomic_begin(); // file sober.c line 60 function main tmp_guard8=((!__unbuffered_prod_done) || (__unbuffered_condVariable!=2)); // file sober.c line 60 function main // ATOMIC_END __CPROVER_atomic_end(); // file sober.c line 60 function main assert(tmp_guard8); // file sober.c line 61 function main return nondet_int(); // file sober.c line 61 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.c line 1 isIdling=(_Bool)(0); // file sober.c line 2 hasWork=(_Bool)(0); // file sober.c line 3 __unbuffered_condVariable=0; // file sober.c line 41 __unbuffered_prod_done=(_Bool)(0); }