file checkiftrans.c: Parsing Converting Type-checking checkiftrans Generating GOTO Program Adding CPROVER library Function Pointer Removal Partial Inlining Generic Property Instrumentation Starting Bounded Model Checking size of program expression: 168 assignments simple slicing removed 1 assignments Generated 18 VCC(s), 16 remaining after simplification Passing problem to propositional reduction Running propositional reduction Solving with MiniSAT2 without simplifier 4067 variables, 11460 clauses SAT checker: negated claim is SATISFIABLE, i.e., does not hold Runtime decision procedure: 0.095s Building error trace Counterexample: State 2 file /usr/include/stdio.h line 169 thread 0 ---------------------------------------------------- stdin=NULL (00000000000000000000000000000000) State 3 file /usr/include/stdio.h line 170 thread 0 ---------------------------------------------------- stdout=NULL (00000000000000000000000000000000) State 4 file /usr/include/stdio.h line 171 thread 0 ---------------------------------------------------- stderr=NULL (00000000000000000000000000000000) State 5 file line 23 thread 0 ---------------------------------------------------- __CPROVER_memory=(assignment removed) State 6 file line 25 thread 0 ---------------------------------------------------- __CPROVER_deallocated=NULL (00000000000000000000000000000000) State 7 file line 26 thread 0 ---------------------------------------------------- __CPROVER_malloc_object=NULL (00000000000000000000000000000000) State 8 file line 27 thread 0 ---------------------------------------------------- __CPROVER_malloc_size=0 (00000000000000000000000000000000) State 9 file line 36 thread 0 ---------------------------------------------------- __CPROVER_rounding_mode=0 (00000000000000000000000000000000) State 10 file /usr/include/i386-linux-gnu/bits/sys_errlist.h line 27 thread 0 ---------------------------------------------------- sys_nerr=0 (00000000000000000000000000000000) State 11 file checkiftrans.c line 3 thread 0 ---------------------------------------------------- jiffies=0 (00000000000000000000000000000000) State 12 file checkiftrans.c line 13 thread 0 ---------------------------------------------------- t1={ .boost_kthread_status=0, .rcu_wake_cond_been_called=0 } ({ 00000000000000000000000000000000, 00000000000000000000000000000000 }) State 13 file checkiftrans.c line 14 thread 0 ---------------------------------------------------- t2={ .boost_kthread_status=0, .rcu_wake_cond_been_called=0 } ({ 00000000000000000000000000000000, 00000000000000000000000000000000 }) State 14 file checkiftrans.c line 27 thread 0 ---------------------------------------------------- rn1={ .exp_tasks=NULL, .gp_tasks=NULL, .boost_tasks=NULL, .qsmask=0, .boost_time=0, .boost_kthread_status=0, .boost_kthread_task=NULL, .rcu_initiate_boost_trace_been_called=0 } ({ 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000 }) State 15 file checkiftrans.c line 28 thread 0 ---------------------------------------------------- rn2={ .exp_tasks=NULL, .gp_tasks=NULL, .boost_tasks=NULL, .qsmask=0, .boost_time=0, .boost_kthread_status=0, .boost_kthread_task=NULL, .rcu_initiate_boost_trace_been_called=0 } ({ 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000 }) State 18 thread 0 ---------------------------------------------------- c::argv'=(assignment removed) State 20 thread 0 ---------------------------------------------------- main::argc=16 (00000000000000000000000000010000) State 21 thread 0 ---------------------------------------------------- main::argv=&argv[0] (00000010000000000000000000000000) State 23 file checkiftrans.c line 114 function main thread 0 ---------------------------------------------------- initialize::argv=&argv[0] (00000010000000000000000000000000) State 24 file checkiftrans.c line 114 function main thread 0 ---------------------------------------------------- initialize::t=&t1.boost_kthread_status (00000011000000000000000000000000) State 25 file checkiftrans.c line 114 function main thread 0 ---------------------------------------------------- initialize::rnp=&rn1.exp_tasks (00000100000000000000000000000000) State 26 file checkiftrans.c line 43 function initialize thread 0 ---------------------------------------------------- rn1={ .exp_tasks=NULL, .gp_tasks=NULL, .boost_tasks=NULL, .qsmask=0, .boost_time=0, .boost_kthread_status=0, .boost_kthread_task=NULL, .rcu_initiate_boost_trace_been_called=0 } ({ 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000 }) State 27 file checkiftrans.c line 44 function initialize thread 0 ---------------------------------------------------- rn1={ .exp_tasks=NULL, .gp_tasks=NULL + 32, .boost_tasks=NULL, .qsmask=0, .boost_time=0, .boost_kthread_status=0, .boost_kthread_task=NULL, .rcu_initiate_boost_trace_been_called=0 } ({ 00000000000000000000000000000000, 00000000000000000000000000100000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000 }) State 28 file checkiftrans.c line 45 function initialize thread 0 ---------------------------------------------------- rn1={ .exp_tasks=NULL, .gp_tasks=NULL + 32, .boost_tasks=NULL, .qsmask=0, .boost_time=0, .boost_kthread_status=0, .boost_kthread_task=NULL, .rcu_initiate_boost_trace_been_called=0 } ({ 00000000000000000000000000000000, 00000000000000000000000000100000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000 }) State 29 file checkiftrans.c line 46 function initialize thread 0 ---------------------------------------------------- rn1={ .exp_tasks=NULL, .gp_tasks=NULL + 32, .boost_tasks=NULL, .qsmask=0, .boost_time=0, .boost_kthread_status=0, .boost_kthread_task=NULL, .rcu_initiate_boost_trace_been_called=0 } ({ 00000000000000000000000000000000, 00000000000000000000000000100000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000 }) State 30 file checkiftrans.c line 47 function initialize thread 0 ---------------------------------------------------- rn1={ .exp_tasks=NULL, .gp_tasks=NULL + 32, .boost_tasks=NULL, .qsmask=0, .boost_time=3, .boost_kthread_status=0, .boost_kthread_task=NULL, .rcu_initiate_boost_trace_been_called=0 } ({ 00000000000000000000000000000000, 00000000000000000000000000100000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000011, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000 }) State 31 file checkiftrans.c line 48 function initialize thread 0 ---------------------------------------------------- rn1={ .exp_tasks=NULL, .gp_tasks=NULL + 32, .boost_tasks=NULL, .qsmask=0, .boost_time=3, .boost_kthread_status=0, .boost_kthread_task=NULL, .rcu_initiate_boost_trace_been_called=0 } ({ 00000000000000000000000000000000, 00000000000000000000000000100000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000011, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000 }) State 32 file checkiftrans.c line 49 function initialize thread 0 ---------------------------------------------------- rn1={ .exp_tasks=NULL, .gp_tasks=NULL + 32, .boost_tasks=NULL, .qsmask=0, .boost_time=3, .boost_kthread_status=0, .boost_kthread_task=&t1.boost_kthread_status, .rcu_initiate_boost_trace_been_called=0 } ({ 00000000000000000000000000000000, 00000000000000000000000000100000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000011, 00000000000000000000000000000000, 00000011000000000000000000000000, 00000000000000000000000000000000 }) State 33 file checkiftrans.c line 50 function initialize thread 0 ---------------------------------------------------- rn1={ .exp_tasks=NULL, .gp_tasks=NULL + 32, .boost_tasks=NULL, .qsmask=0, .boost_time=3, .boost_kthread_status=0, .boost_kthread_task=&t1.boost_kthread_status, .rcu_initiate_boost_trace_been_called=0 } ({ 00000000000000000000000000000000, 00000000000000000000000000100000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000011, 00000000000000000000000000000000, 00000011000000000000000000000000, 00000000000000000000000000000000 }) State 34 file checkiftrans.c line 51 function initialize thread 0 ---------------------------------------------------- t1={ .boost_kthread_status=0, .rcu_wake_cond_been_called=0 } ({ 00000000000000000000000000000000, 00000000000000000000000000000000 }) State 36 file checkiftrans.c line 115 function main thread 0 ---------------------------------------------------- initialize::argv=&argv[0] (00000010000000000000000000000000) State 37 file checkiftrans.c line 115 function main thread 0 ---------------------------------------------------- initialize::t=&t2.boost_kthread_status (00000101000000000000000000000000) State 38 file checkiftrans.c line 115 function main thread 0 ---------------------------------------------------- initialize::rnp=&rn2.exp_tasks (00000110000000000000000000000000) State 39 file checkiftrans.c line 43 function initialize thread 0 ---------------------------------------------------- rn2={ .exp_tasks=NULL, .gp_tasks=NULL, .boost_tasks=NULL, .qsmask=0, .boost_time=0, .boost_kthread_status=0, .boost_kthread_task=NULL, .rcu_initiate_boost_trace_been_called=0 } ({ 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000 }) State 40 file checkiftrans.c line 44 function initialize thread 0 ---------------------------------------------------- rn2={ .exp_tasks=NULL, .gp_tasks=NULL + 32, .boost_tasks=NULL, .qsmask=0, .boost_time=0, .boost_kthread_status=0, .boost_kthread_task=NULL, .rcu_initiate_boost_trace_been_called=0 } ({ 00000000000000000000000000000000, 00000000000000000000000000100000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000 }) State 41 file checkiftrans.c line 45 function initialize thread 0 ---------------------------------------------------- rn2={ .exp_tasks=NULL, .gp_tasks=NULL + 32, .boost_tasks=NULL, .qsmask=0, .boost_time=0, .boost_kthread_status=0, .boost_kthread_task=NULL, .rcu_initiate_boost_trace_been_called=0 } ({ 00000000000000000000000000000000, 00000000000000000000000000100000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000 }) State 42 file checkiftrans.c line 46 function initialize thread 0 ---------------------------------------------------- rn2={ .exp_tasks=NULL, .gp_tasks=NULL + 32, .boost_tasks=NULL, .qsmask=0, .boost_time=0, .boost_kthread_status=0, .boost_kthread_task=NULL, .rcu_initiate_boost_trace_been_called=0 } ({ 00000000000000000000000000000000, 00000000000000000000000000100000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000 }) State 43 file checkiftrans.c line 47 function initialize thread 0 ---------------------------------------------------- rn2={ .exp_tasks=NULL, .gp_tasks=NULL + 32, .boost_tasks=NULL, .qsmask=0, .boost_time=3, .boost_kthread_status=0, .boost_kthread_task=NULL, .rcu_initiate_boost_trace_been_called=0 } ({ 00000000000000000000000000000000, 00000000000000000000000000100000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000011, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000 }) State 44 file checkiftrans.c line 48 function initialize thread 0 ---------------------------------------------------- rn2={ .exp_tasks=NULL, .gp_tasks=NULL + 32, .boost_tasks=NULL, .qsmask=0, .boost_time=3, .boost_kthread_status=0, .boost_kthread_task=NULL, .rcu_initiate_boost_trace_been_called=0 } ({ 00000000000000000000000000000000, 00000000000000000000000000100000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000011, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000 }) State 45 file checkiftrans.c line 49 function initialize thread 0 ---------------------------------------------------- rn2={ .exp_tasks=NULL, .gp_tasks=NULL + 32, .boost_tasks=NULL, .qsmask=0, .boost_time=3, .boost_kthread_status=0, .boost_kthread_task=&t2.boost_kthread_status, .rcu_initiate_boost_trace_been_called=0 } ({ 00000000000000000000000000000000, 00000000000000000000000000100000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000011, 00000000000000000000000000000000, 00000101000000000000000000000000, 00000000000000000000000000000000 }) State 46 file checkiftrans.c line 50 function initialize thread 0 ---------------------------------------------------- rn2={ .exp_tasks=NULL, .gp_tasks=NULL + 32, .boost_tasks=NULL, .qsmask=0, .boost_time=3, .boost_kthread_status=0, .boost_kthread_task=&t2.boost_kthread_status, .rcu_initiate_boost_trace_been_called=0 } ({ 00000000000000000000000000000000, 00000000000000000000000000100000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000011, 00000000000000000000000000000000, 00000101000000000000000000000000, 00000000000000000000000000000000 }) State 47 file checkiftrans.c line 51 function initialize thread 0 ---------------------------------------------------- t2={ .boost_kthread_status=0, .rcu_wake_cond_been_called=0 } ({ 00000000000000000000000000000000, 00000000000000000000000000000000 }) State 57 file checkiftrans.c line 118 function main thread 0 ---------------------------------------------------- do_old_if::argv=&argv[0] (00000010000000000000000000000000) State 58 file checkiftrans.c line 118 function main thread 0 ---------------------------------------------------- do_old_if::t_in=&t1.boost_kthread_status (00000011000000000000000000000000) State 59 file checkiftrans.c line 118 function main thread 0 ---------------------------------------------------- do_old_if::rnp=&rn1.exp_tasks (00000100000000000000000000000000) State 60 file checkiftrans.c line 59 function do_old_if thread 0 ---------------------------------------------------- c::do_old_if::$tmp::tmp_condition$1=FALSE (0) State 62 file checkiftrans.c line 60 function do_old_if thread 0 ---------------------------------------------------- c::do_old_if::$tmp::tmp_condition$5=TRUE (1) State 64 file checkiftrans.c line 61 function do_old_if thread 0 ---------------------------------------------------- c::do_old_if::$tmp::tmp_condition$6=TRUE (1) State 65 file checkiftrans.c line 60 function do_old_if thread 0 ---------------------------------------------------- c::do_old_if::$tmp::tmp_condition$4=TRUE (1) State 67 file checkiftrans.c line 62 function do_old_if thread 0 ---------------------------------------------------- c::do_old_if::$tmp::tmp_condition$7=TRUE (1) State 68 file checkiftrans.c line 61 function do_old_if thread 0 ---------------------------------------------------- c::do_old_if::$tmp::tmp_condition$3=TRUE (1) State 70 file checkiftrans.c line 63 function do_old_if thread 0 ---------------------------------------------------- c::do_old_if::$tmp::tmp_condition$8=FALSE (0) State 71 file checkiftrans.c line 62 function do_old_if thread 0 ---------------------------------------------------- c::do_old_if::$tmp::tmp_condition$2=FALSE (0) State 74 file checkiftrans.c line 71 function do_old_if thread 0 ---------------------------------------------------- rcu_initiate_boost_trace::rnp=&rn1.exp_tasks (00000100000000000000000000000000) State 75 file checkiftrans.c line 38 function rcu_initiate_boost_trace thread 0 ---------------------------------------------------- rn1={ .exp_tasks=NULL, .gp_tasks=NULL + 32, .boost_tasks=NULL, .qsmask=0, .boost_time=3, .boost_kthread_status=0, .boost_kthread_task=&t1.boost_kthread_status, .rcu_initiate_boost_trace_been_called=1 } ({ 00000000000000000000000000000000, 00000000000000000000000000100000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000011, 00000000000000000000000000000000, 00000011000000000000000000000000, 00000000000000000000000000000001 }) State 77 file checkiftrans.c line 119 function main thread 0 ---------------------------------------------------- do_new_if::argv=&argv[0] (00000010000000000000000000000000) State 78 file checkiftrans.c line 119 function main thread 0 ---------------------------------------------------- do_new_if::t_in=&t2.boost_kthread_status (00000101000000000000000000000000) State 79 file checkiftrans.c line 119 function main thread 0 ---------------------------------------------------- do_new_if::rnp=&rn2.exp_tasks (00000110000000000000000000000000) State 80 file checkiftrans.c line 81 function do_new_if thread 0 ---------------------------------------------------- c::do_new_if::$tmp::tmp_condition$1=TRUE (1) State 82 file checkiftrans.c line 82 function do_new_if thread 0 ---------------------------------------------------- c::do_new_if::$tmp::tmp_condition$4=FALSE (0) State 84 file checkiftrans.c line 83 function do_new_if thread 0 ---------------------------------------------------- c::do_new_if::$tmp::tmp_condition$5=FALSE (0) State 85 file checkiftrans.c line 82 function do_new_if thread 0 ---------------------------------------------------- c::do_new_if::$tmp::tmp_condition$3=FALSE (0) State 87 file checkiftrans.c line 84 function do_new_if thread 0 ---------------------------------------------------- c::do_new_if::$tmp::tmp_condition$7=FALSE (0) State 89 file checkiftrans.c line 84 function do_new_if thread 0 ---------------------------------------------------- c::do_new_if::$tmp::tmp_condition$6=FALSE (0) State 90 file checkiftrans.c line 83 function do_new_if thread 0 ---------------------------------------------------- c::do_new_if::$tmp::tmp_condition$2=FALSE (0) State 93 file checkiftrans.c line 90 function do_new_if thread 0 ---------------------------------------------------- rn2={ .exp_tasks=NULL, .gp_tasks=NULL + 32, .boost_tasks=NULL + 32, .qsmask=0, .boost_time=3, .boost_kthread_status=0, .boost_kthread_task=&t2.boost_kthread_status, .rcu_initiate_boost_trace_been_called=0 } ({ 00000000000000000000000000000000, 00000000000000000000000000100000, 00000000000000000000000000100000, 00000000000000000000000000000000, 00000000000000000000000000000011, 00000000000000000000000000000000, 00000101000000000000000000000000, 00000000000000000000000000000000 }) State 94 file checkiftrans.c line 92 function do_new_if thread 0 ---------------------------------------------------- do_new_if::1::t=&t2.boost_kthread_status (00000101000000000000000000000000) State 97 file checkiftrans.c line 94 function do_new_if thread 0 ---------------------------------------------------- rcu_wake_cond::t=&t2.boost_kthread_status (00000101000000000000000000000000) State 98 file checkiftrans.c line 94 function do_new_if thread 0 ---------------------------------------------------- rcu_wake_cond::bks=0 (00000000000000000000000000000000) State 99 file checkiftrans.c line 32 function rcu_wake_cond thread 0 ---------------------------------------------------- t2={ .boost_kthread_status=0, .rcu_wake_cond_been_called=1 } ({ 00000000000000000000000000000000, 00000000000000000000000000000001 }) State 100 file checkiftrans.c line 33 function rcu_wake_cond thread 0 ---------------------------------------------------- t2={ .boost_kthread_status=0, .rcu_wake_cond_been_called=1 } ({ 00000000000000000000000000000000, 00000000000000000000000000000001 }) Violated property: file checkiftrans.c line 102 function check assertion rn1.boost_tasks == rn2.boost_tasks VERIFICATION FAILED