file checkiftrans.c: Parsing Converting Type-checking checkiftrans file checkiftrans.c line 60 function do_old_if: function `c::ULONG_CMP_GE' is not declared file checkiftrans.c line 82 function do_new_if: function `c::ULONG_CMP_LT' is not declared Generating GOTO Program Adding CPROVER library Function Pointer Removal Partial Inlining Generic Property Instrumentation Starting Bounded Model Checking **** WARNING: no body for function c::ULONG_CMP_GE **** WARNING: no body for function c::ULONG_CMP_LT size of program expression: 177 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 4471 variables, 12303 clauses SAT checker: negated claim is SATISFIABLE, i.e., does not hold Runtime decision procedure: 0.079s 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 10 thread 0 ---------------------------------------------------- t1={ .boost_kthread_status=0, .rcu_wake_cond_been_called=0 } ({ 00000000000000000000000000000000, 00000000000000000000000000000000 }) State 13 file checkiftrans.c line 11 thread 0 ---------------------------------------------------- t2={ .boost_kthread_status=0, .rcu_wake_cond_been_called=0 } ({ 00000000000000000000000000000000, 00000000000000000000000000000000 }) State 14 file checkiftrans.c line 24 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 25 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=514 (00000000000000000000001000000010) State 21 thread 0 ---------------------------------------------------- main::argv=&argv[0] (00000010000000000000000000000000) State 23 file checkiftrans.c line 111 function main thread 0 ---------------------------------------------------- initialize::argv=&argv[0] (00000010000000000000000000000000) State 24 file checkiftrans.c line 111 function main thread 0 ---------------------------------------------------- initialize::t=&t1.boost_kthread_status (00000011000000000000000000000000) State 25 file checkiftrans.c line 111 function main thread 0 ---------------------------------------------------- initialize::rnp=&rn1.exp_tasks (00000100000000000000000000000000) State 26 file checkiftrans.c line 40 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 41 function initialize thread 0 ---------------------------------------------------- rn1={ .exp_tasks=NULL, .gp_tasks=NULL + 2097152, .boost_tasks=NULL, .qsmask=0, .boost_time=0, .boost_kthread_status=0, .boost_kthread_task=NULL, .rcu_initiate_boost_trace_been_called=0 } ({ 00000000000000000000000000000000, 00000000001000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000 }) State 28 file checkiftrans.c line 42 function initialize thread 0 ---------------------------------------------------- rn1={ .exp_tasks=NULL, .gp_tasks=NULL + 2097152, .boost_tasks=NULL, .qsmask=0, .boost_time=0, .boost_kthread_status=0, .boost_kthread_task=NULL, .rcu_initiate_boost_trace_been_called=0 } ({ 00000000000000000000000000000000, 00000000001000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000 }) State 29 file checkiftrans.c line 43 function initialize thread 0 ---------------------------------------------------- rn1={ .exp_tasks=NULL, .gp_tasks=NULL + 2097152, .boost_tasks=NULL, .qsmask=0, .boost_time=0, .boost_kthread_status=0, .boost_kthread_task=NULL, .rcu_initiate_boost_trace_been_called=0 } ({ 00000000000000000000000000000000, 00000000001000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000 }) State 30 file checkiftrans.c line 44 function initialize thread 0 ---------------------------------------------------- rn1={ .exp_tasks=NULL, .gp_tasks=NULL + 2097152, .boost_tasks=NULL, .qsmask=0, .boost_time=0, .boost_kthread_status=0, .boost_kthread_task=NULL, .rcu_initiate_boost_trace_been_called=0 } ({ 00000000000000000000000000000000, 00000000001000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000 }) State 31 file checkiftrans.c line 45 function initialize thread 0 ---------------------------------------------------- rn1={ .exp_tasks=NULL, .gp_tasks=NULL + 2097152, .boost_tasks=NULL, .qsmask=0, .boost_time=0, .boost_kthread_status=0, .boost_kthread_task=NULL, .rcu_initiate_boost_trace_been_called=0 } ({ 00000000000000000000000000000000, 00000000001000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000 }) State 32 file checkiftrans.c line 46 function initialize thread 0 ---------------------------------------------------- rn1={ .exp_tasks=NULL, .gp_tasks=NULL + 2097152, .boost_tasks=NULL, .qsmask=0, .boost_time=0, .boost_kthread_status=0, .boost_kthread_task=&t1.boost_kthread_status, .rcu_initiate_boost_trace_been_called=0 } ({ 00000000000000000000000000000000, 00000000001000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000011000000000000000000000000, 00000000000000000000000000000000 }) State 33 file checkiftrans.c line 47 function initialize thread 0 ---------------------------------------------------- rn1={ .exp_tasks=NULL, .gp_tasks=NULL + 2097152, .boost_tasks=NULL, .qsmask=0, .boost_time=0, .boost_kthread_status=0, .boost_kthread_task=&t1.boost_kthread_status, .rcu_initiate_boost_trace_been_called=0 } ({ 00000000000000000000000000000000, 00000000001000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000011000000000000000000000000, 00000000000000000000000000000000 }) State 34 file checkiftrans.c line 48 function initialize thread 0 ---------------------------------------------------- t1={ .boost_kthread_status=0, .rcu_wake_cond_been_called=0 } ({ 00000000000000000000000000000000, 00000000000000000000000000000000 }) State 36 file checkiftrans.c line 112 function main thread 0 ---------------------------------------------------- initialize::argv=&argv[0] (00000010000000000000000000000000) State 37 file checkiftrans.c line 112 function main thread 0 ---------------------------------------------------- initialize::t=&t2.boost_kthread_status (00000101000000000000000000000000) State 38 file checkiftrans.c line 112 function main thread 0 ---------------------------------------------------- initialize::rnp=&rn2.exp_tasks (00000110000000000000000000000000) State 39 file checkiftrans.c line 40 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 41 function initialize thread 0 ---------------------------------------------------- rn2={ .exp_tasks=NULL, .gp_tasks=NULL + 2097152, .boost_tasks=NULL, .qsmask=0, .boost_time=0, .boost_kthread_status=0, .boost_kthread_task=NULL, .rcu_initiate_boost_trace_been_called=0 } ({ 00000000000000000000000000000000, 00000000001000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000 }) State 41 file checkiftrans.c line 42 function initialize thread 0 ---------------------------------------------------- rn2={ .exp_tasks=NULL, .gp_tasks=NULL + 2097152, .boost_tasks=NULL, .qsmask=0, .boost_time=0, .boost_kthread_status=0, .boost_kthread_task=NULL, .rcu_initiate_boost_trace_been_called=0 } ({ 00000000000000000000000000000000, 00000000001000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000 }) State 42 file checkiftrans.c line 43 function initialize thread 0 ---------------------------------------------------- rn2={ .exp_tasks=NULL, .gp_tasks=NULL + 2097152, .boost_tasks=NULL, .qsmask=0, .boost_time=0, .boost_kthread_status=0, .boost_kthread_task=NULL, .rcu_initiate_boost_trace_been_called=0 } ({ 00000000000000000000000000000000, 00000000001000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000 }) State 43 file checkiftrans.c line 44 function initialize thread 0 ---------------------------------------------------- rn2={ .exp_tasks=NULL, .gp_tasks=NULL + 2097152, .boost_tasks=NULL, .qsmask=0, .boost_time=0, .boost_kthread_status=0, .boost_kthread_task=NULL, .rcu_initiate_boost_trace_been_called=0 } ({ 00000000000000000000000000000000, 00000000001000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000 }) State 44 file checkiftrans.c line 45 function initialize thread 0 ---------------------------------------------------- rn2={ .exp_tasks=NULL, .gp_tasks=NULL + 2097152, .boost_tasks=NULL, .qsmask=0, .boost_time=0, .boost_kthread_status=0, .boost_kthread_task=NULL, .rcu_initiate_boost_trace_been_called=0 } ({ 00000000000000000000000000000000, 00000000001000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000 }) State 45 file checkiftrans.c line 46 function initialize thread 0 ---------------------------------------------------- rn2={ .exp_tasks=NULL, .gp_tasks=NULL + 2097152, .boost_tasks=NULL, .qsmask=0, .boost_time=0, .boost_kthread_status=0, .boost_kthread_task=&t2.boost_kthread_status, .rcu_initiate_boost_trace_been_called=0 } ({ 00000000000000000000000000000000, 00000000001000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000101000000000000000000000000, 00000000000000000000000000000000 }) State 46 file checkiftrans.c line 47 function initialize thread 0 ---------------------------------------------------- rn2={ .exp_tasks=NULL, .gp_tasks=NULL + 2097152, .boost_tasks=NULL, .qsmask=0, .boost_time=0, .boost_kthread_status=0, .boost_kthread_task=&t2.boost_kthread_status, .rcu_initiate_boost_trace_been_called=0 } ({ 00000000000000000000000000000000, 00000000001000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000101000000000000000000000000, 00000000000000000000000000000000 }) State 47 file checkiftrans.c line 48 function initialize thread 0 ---------------------------------------------------- t2={ .boost_kthread_status=0, .rcu_wake_cond_been_called=0 } ({ 00000000000000000000000000000000, 00000000000000000000000000000000 }) State 57 file checkiftrans.c line 115 function main thread 0 ---------------------------------------------------- do_old_if::argv=&argv[0] (00000010000000000000000000000000) State 58 file checkiftrans.c line 115 function main thread 0 ---------------------------------------------------- do_old_if::t_in=&t1.boost_kthread_status (00000011000000000000000000000000) State 59 file checkiftrans.c line 115 function main thread 0 ---------------------------------------------------- do_old_if::rnp=&rn1.exp_tasks (00000100000000000000000000000000) State 60 file checkiftrans.c line 56 function do_old_if thread 0 ---------------------------------------------------- c::do_old_if::$tmp::tmp_condition$1=FALSE (0) State 62 file checkiftrans.c line 57 function do_old_if thread 0 ---------------------------------------------------- c::do_old_if::$tmp::tmp_condition$5=TRUE (1) State 64 file checkiftrans.c line 58 function do_old_if thread 0 ---------------------------------------------------- c::do_old_if::$tmp::tmp_condition$6=TRUE (1) State 65 file checkiftrans.c line 57 function do_old_if thread 0 ---------------------------------------------------- c::do_old_if::$tmp::tmp_condition$4=TRUE (1) State 67 file checkiftrans.c line 59 function do_old_if thread 0 ---------------------------------------------------- c::do_old_if::$tmp::tmp_condition$7=TRUE (1) State 68 file checkiftrans.c line 58 function do_old_if thread 0 ---------------------------------------------------- c::do_old_if::$tmp::tmp_condition$3=TRUE (1) State 71 file checkiftrans.c line 60 function do_old_if thread 0 ---------------------------------------------------- c::do_old_if::$tmp::return_value_ULONG_CMP_GE$9=0 (00000000000000000000000000000000) State 72 file checkiftrans.c line 60 function do_old_if thread 0 ---------------------------------------------------- c::do_old_if::$tmp::tmp_condition$8=FALSE (0) State 73 file checkiftrans.c line 59 function do_old_if thread 0 ---------------------------------------------------- c::do_old_if::$tmp::tmp_condition$2=FALSE (0) State 76 file checkiftrans.c line 68 function do_old_if thread 0 ---------------------------------------------------- rcu_initiate_boost_trace::rnp=&rn1.exp_tasks (00000100000000000000000000000000) State 77 file checkiftrans.c line 35 function rcu_initiate_boost_trace thread 0 ---------------------------------------------------- rn1={ .exp_tasks=NULL, .gp_tasks=NULL + 2097152, .boost_tasks=NULL, .qsmask=0, .boost_time=0, .boost_kthread_status=0, .boost_kthread_task=&t1.boost_kthread_status, .rcu_initiate_boost_trace_been_called=1 } ({ 00000000000000000000000000000000, 00000000001000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000011000000000000000000000000, 00000000000000000000000000000001 }) State 79 file checkiftrans.c line 116 function main thread 0 ---------------------------------------------------- do_new_if::argv=&argv[0] (00000010000000000000000000000000) State 80 file checkiftrans.c line 116 function main thread 0 ---------------------------------------------------- do_new_if::t_in=&t2.boost_kthread_status (00000101000000000000000000000000) State 81 file checkiftrans.c line 116 function main thread 0 ---------------------------------------------------- do_new_if::rnp=&rn2.exp_tasks (00000110000000000000000000000000) State 82 file checkiftrans.c line 78 function do_new_if thread 0 ---------------------------------------------------- c::do_new_if::$tmp::tmp_condition$1=TRUE (1) State 84 file checkiftrans.c line 79 function do_new_if thread 0 ---------------------------------------------------- c::do_new_if::$tmp::tmp_condition$4=FALSE (0) State 86 file checkiftrans.c line 80 function do_new_if thread 0 ---------------------------------------------------- c::do_new_if::$tmp::tmp_condition$5=FALSE (0) State 87 file checkiftrans.c line 79 function do_new_if thread 0 ---------------------------------------------------- c::do_new_if::$tmp::tmp_condition$3=FALSE (0) State 89 file checkiftrans.c line 81 function do_new_if thread 0 ---------------------------------------------------- c::do_new_if::$tmp::tmp_condition$7=FALSE (0) State 91 file checkiftrans.c line 81 function do_new_if thread 0 ---------------------------------------------------- c::do_new_if::$tmp::tmp_condition$6=FALSE (0) State 92 file checkiftrans.c line 80 function do_new_if thread 0 ---------------------------------------------------- c::do_new_if::$tmp::tmp_condition$2=FALSE (0) State 95 file checkiftrans.c line 87 function do_new_if thread 0 ---------------------------------------------------- rn2={ .exp_tasks=NULL, .gp_tasks=NULL + 2097152, .boost_tasks=NULL + 2097152, .qsmask=0, .boost_time=0, .boost_kthread_status=0, .boost_kthread_task=&t2.boost_kthread_status, .rcu_initiate_boost_trace_been_called=0 } ({ 00000000000000000000000000000000, 00000000001000000000000000000000, 00000000001000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000000000000000000000000000000, 00000101000000000000000000000000, 00000000000000000000000000000000 }) State 96 file checkiftrans.c line 89 function do_new_if thread 0 ---------------------------------------------------- do_new_if::1::t=&t2.boost_kthread_status (00000101000000000000000000000000) State 99 file checkiftrans.c line 91 function do_new_if thread 0 ---------------------------------------------------- rcu_wake_cond::t=&t2.boost_kthread_status (00000101000000000000000000000000) State 100 file checkiftrans.c line 91 function do_new_if thread 0 ---------------------------------------------------- rcu_wake_cond::bks=0 (00000000000000000000000000000000) State 101 file checkiftrans.c line 29 function rcu_wake_cond thread 0 ---------------------------------------------------- t2={ .boost_kthread_status=0, .rcu_wake_cond_been_called=1 } ({ 00000000000000000000000000000000, 00000000000000000000000000000001 }) State 102 file checkiftrans.c line 30 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 99 function check assertion rn1.boost_tasks == rn2.boost_tasks VERIFICATION FAILED