// 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::hasWork$w_buff0 // _Bool chasWorkw_buff0; // c::hasWork$w_buff1 // _Bool chasWorkw_buff1; // c::hasWork$w_buff0_used // _Bool chasWorkw_buff0_used; // c::hasWork$w_buff1_used // _Bool chasWorkw_buff1_used; // c::hasWork$mem_tmp // _Bool chasWorkmem_tmp; // c::hasWork$flush_delayed // _Bool chasWorkflush_delayed; // c::hasWork$read_delayed // _Bool chasWorkread_delayed; // c::hasWork$read_delayed_var // _Bool * chasWorkread_delayed_var; // c::hasWork$r_buff0_thd0 // _Bool chasWorkr_buff0_thd0; // c::hasWork$r_buff1_thd0 // _Bool chasWorkr_buff1_thd0; // c::hasWork$r_buff0_thd1 // _Bool chasWorkr_buff0_thd1; // c::hasWork$r_buff1_thd1 // _Bool chasWorkr_buff1_thd1; // c::hasWork$r_buff0_thd2 // _Bool chasWorkr_buff0_thd2; // c::hasWork$r_buff1_thd2 // _Bool chasWorkr_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) { chasWorkw_buff0_used=false; chasWorkw_buff1_used=false; chasWorkflush_delayed=false; chasWorkread_delayed=false; chasWorkread_delayed_var=0; chasWorkr_buff0_thd0=false; chasWorkr_buff0_thd1=false; chasWorkr_buff0_thd2=false; chasWorkr_buff1_thd0=false; chasWorkr_buff1_thd1=false; chasWorkr_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 isIdling=(_Bool)(1); // 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 weakchoice0=nondet_bool(); // file sober.c line 35 function BlockOnIdle weakchoice2=nondet_bool(); // file sober.c line 35 function BlockOnIdle chasWorkflush_delayed=weakchoice2; // file sober.c line 35 function BlockOnIdle chasWorkmem_tmp=hasWork; // file sober.c line 35 function BlockOnIdle hasWork=(((!chasWorkw_buff0_used) || (((!chasWorkr_buff0_thd1) && (!chasWorkw_buff1_used)) || ((!chasWorkr_buff0_thd1) && (!chasWorkr_buff1_thd1))))? hasWork:((chasWorkw_buff0_used && chasWorkr_buff0_thd1)? chasWorkw_buff0:chasWorkw_buff1)); // file sober.c line 35 function BlockOnIdle chasWorkw_buff0=(weakchoice2? chasWorkw_buff0:(((!chasWorkw_buff0_used) || (((!chasWorkr_buff0_thd1) && (!chasWorkw_buff1_used)) || ((!chasWorkr_buff0_thd1) && (!chasWorkr_buff1_thd1))))? chasWorkw_buff0:((chasWorkw_buff0_used && chasWorkr_buff0_thd1)? chasWorkw_buff0:chasWorkw_buff0))); // file sober.c line 35 function BlockOnIdle chasWorkw_buff1=(weakchoice2? chasWorkw_buff1:(((!chasWorkw_buff0_used) || (((!chasWorkr_buff0_thd1) && (!chasWorkw_buff1_used)) || ((!chasWorkr_buff0_thd1) && (!chasWorkr_buff1_thd1))))? chasWorkw_buff1:((chasWorkw_buff0_used && chasWorkr_buff0_thd1)? chasWorkw_buff1:chasWorkw_buff1))); // file sober.c line 35 function BlockOnIdle chasWorkw_buff0_used=(weakchoice2? chasWorkw_buff0_used:(((!chasWorkw_buff0_used) || (((!chasWorkr_buff0_thd1) && (!chasWorkw_buff1_used)) || ((!chasWorkr_buff0_thd1) && (!chasWorkr_buff1_thd1))))? chasWorkw_buff0_used:((chasWorkw_buff0_used && chasWorkr_buff0_thd1)? false:chasWorkw_buff0_used))); // file sober.c line 35 function BlockOnIdle chasWorkw_buff1_used=(weakchoice2? chasWorkw_buff1_used:(((!chasWorkw_buff0_used) || (((!chasWorkr_buff0_thd1) && (!chasWorkw_buff1_used)) || ((!chasWorkr_buff0_thd1) && (!chasWorkr_buff1_thd1))))? chasWorkw_buff1_used:((chasWorkw_buff0_used && chasWorkr_buff0_thd1)? false:false))); // file sober.c line 35 function BlockOnIdle chasWorkr_buff0_thd1=(weakchoice2? chasWorkr_buff0_thd1:(((!chasWorkw_buff0_used) || (((!chasWorkr_buff0_thd1) && (!chasWorkw_buff1_used)) || ((!chasWorkr_buff0_thd1) && (!chasWorkr_buff1_thd1))))? chasWorkr_buff0_thd1:((chasWorkw_buff0_used && chasWorkr_buff0_thd1)? false:chasWorkr_buff0_thd1))); // file sober.c line 35 function BlockOnIdle chasWorkr_buff1_thd1=(weakchoice2? chasWorkr_buff1_thd1:(((!chasWorkw_buff0_used) || (((!chasWorkr_buff0_thd1) && (!chasWorkw_buff1_used)) || ((!chasWorkr_buff0_thd1) && (!chasWorkr_buff1_thd1))))? chasWorkr_buff1_thd1:((chasWorkw_buff0_used && chasWorkr_buff0_thd1)? false:false))); // file sober.c line 35 function BlockOnIdle tmp_guard1=(!(!hasWork)); // file sober.c line 35 function BlockOnIdle hasWork=(chasWorkflush_delayed? chasWorkmem_tmp:hasWork); // file sober.c line 35 function BlockOnIdle chasWorkflush_delayed=false; // 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 chasWorkw_buff1=chasWorkw_buff0; // file sober.c line 46 function NotifyPotentialWork chasWorkw_buff0=(_Bool)(1); // file sober.c line 46 function NotifyPotentialWork chasWorkw_buff1_used=chasWorkw_buff0_used; // file sober.c line 46 function NotifyPotentialWork chasWorkw_buff0_used=true; // file sober.c line 46 function NotifyPotentialWork assert((!(chasWorkw_buff1_used && chasWorkw_buff0_used))); // file sober.c line 46 function NotifyPotentialWork chasWorkr_buff1_thd0=chasWorkr_buff0_thd0; // file sober.c line 46 function NotifyPotentialWork chasWorkr_buff1_thd1=chasWorkr_buff0_thd1; // file sober.c line 46 function NotifyPotentialWork chasWorkr_buff1_thd2=chasWorkr_buff0_thd2; // file sober.c line 46 function NotifyPotentialWork chasWorkr_buff0_thd2=true; // 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 tmp_guard5=(!isIdling); // 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); }