CBMC version 5.0 64-bit linux Parsing fake.c Converting Type-checking fake Generating GOTO Program Adding CPROVER library Function Pointer Removal Partial Inlining Generic Property Instrumentation Starting Bounded Model Checking Adding SC constraints size of program expression: 13477 steps no slicing due to threads Generated 35 VCC(s), 34 remaining after simplification Passing problem to propositional reduction Running propositional reduction Post-processing Solving with MiniSAT 2.2.0 with simplifier 185627 variables, 815691 clauses SAT checker: negated claim is SATISFIABLE, i.e., does not hold Runtime decision procedure: 16.23s Building error trace Counterexample: State 32 thread 0 ---------------------------------------------------- argv'[134217728]=irep("(\"nil\")")[134217728] (?) State 35 file fake.c line 179 thread 0 ---------------------------------------------------- argc=134217728 (00001000000000000000000000000000) State 36 file fake.c line 179 thread 0 ---------------------------------------------------- argv=argv' (0000010000000000000000000000000000000000000000000000000000000000) State 37 file fake.c line 181 function main thread 0 ---------------------------------------------------- tu=0 (0000000000000000000000000000000000000000000000000000000000000000) State 38 file fake.c line 182 function main thread 0 ---------------------------------------------------- tpr=0 (0000000000000000000000000000000000000000000000000000000000000000) State 41 file tiny.c line 86 function rcu_idle_enter thread 0 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 42 file tiny.c line 87 function rcu_idle_enter thread 0 ---------------------------------------------------- newval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 45 file tiny.c line 89 function rcu_idle_enter thread 0 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 48 file fake.c line 97 function local_irq_save thread 0 ---------------------------------------------------- local_irq_depth=1 (00000000000000000000000000000001) State 65 file tiny.c line 93 function rcu_idle_enter thread 0 ---------------------------------------------------- newval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 69 file tiny.c line 96 function rcu_idle_enter thread 0 ---------------------------------------------------- newval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 74 file tiny.c line 222 function rcu_sched_qs thread 0 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 77 file tiny.c line 224 function rcu_sched_qs thread 0 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 80 file fake.c line 97 function local_irq_save thread 0 ---------------------------------------------------- local_irq_depth=2 (00000000000000000000000000000010) State 86 file tiny.c line 225 function rcu_sched_qs thread 0 ---------------------------------------------------- rcp=&rcu_sched_ctrlblk.rcucblist (0000001000000000000000000000000000000000000000000000000000000000) State 95 file tiny.c line 226 function rcu_sched_qs thread 0 ---------------------------------------------------- rcp=&rcu_bh_ctrlblk.rcucblist (0000001100000000000000000000000000000000000000000000000000000000) State 104 file tiny.c line 228 function rcu_sched_qs thread 0 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 105 file fake.c line 110 function local_irq_restore thread 0 ---------------------------------------------------- local_irq_depth=1 (00000000000000000000000000000001) State 109 file tiny.c line 77 function rcu_idle_enter_common thread 0 ---------------------------------------------------- rcu_dynticks_nesting=0 (0000000000000000000000000000000000000000000000000000000000000000) State 113 file tiny.c line 97 function rcu_idle_enter thread 0 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 114 file fake.c line 110 function local_irq_restore thread 0 ---------------------------------------------------- local_irq_depth=0 (00000000000000000000000000000000) State 222 file tiny.c line 143 function rcu_idle_exit thread 2 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 223 file tiny.c line 144 function rcu_idle_exit thread 2 ---------------------------------------------------- oldval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 226 file tiny.c line 146 function rcu_idle_exit thread 2 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 229 file fake.c line 97 function local_irq_save thread 2 ---------------------------------------------------- local_irq_depth=1 (00000000000000000000000000000001) State 241 file tiny.c line 147 function rcu_idle_exit thread 2 ---------------------------------------------------- oldval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 249 file tiny.c line 152 function rcu_idle_exit thread 2 ---------------------------------------------------- rcu_dynticks_nesting=90071992547409920 (0000000101000000000000000000000000000000000000000000000000000000) State 252 file tiny.c line 153 function rcu_idle_exit thread 2 ---------------------------------------------------- oldval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 258 file tiny.c line 154 function rcu_idle_exit thread 2 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 259 file fake.c line 110 function local_irq_restore thread 2 ---------------------------------------------------- local_irq_depth=0 (00000000000000000000000000000000) State 279 file fake.c line 134 function rcu_reader thread 2 ---------------------------------------------------- __unbuffered_tpr_x=0 (00000000000000000000000000000000) State 290 file tiny.c line 86 function rcu_idle_enter thread 2 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 291 file tiny.c line 87 function rcu_idle_enter thread 2 ---------------------------------------------------- newval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 294 file tiny.c line 89 function rcu_idle_enter thread 2 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 297 file fake.c line 97 function local_irq_save thread 2 ---------------------------------------------------- local_irq_depth=1 (00000000000000000000000000000001) State 316 file tiny.c line 93 function rcu_idle_enter thread 2 ---------------------------------------------------- newval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 320 file tiny.c line 96 function rcu_idle_enter thread 2 ---------------------------------------------------- newval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 325 file tiny.c line 222 function rcu_sched_qs thread 2 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 328 file tiny.c line 224 function rcu_sched_qs thread 2 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 331 file fake.c line 97 function local_irq_save thread 2 ---------------------------------------------------- local_irq_depth=2 (00000000000000000000000000000010) State 337 file tiny.c line 225 function rcu_sched_qs thread 2 ---------------------------------------------------- rcp=&rcu_sched_ctrlblk.rcucblist (0000001000000000000000000000000000000000000000000000000000000000) State 346 file tiny.c line 226 function rcu_sched_qs thread 2 ---------------------------------------------------- rcp=&rcu_bh_ctrlblk.rcucblist (0000001100000000000000000000000000000000000000000000000000000000) State 355 file tiny.c line 228 function rcu_sched_qs thread 2 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 356 file fake.c line 110 function local_irq_restore thread 2 ---------------------------------------------------- local_irq_depth=1 (00000000000000000000000000000001) State 360 file tiny.c line 77 function rcu_idle_enter_common thread 2 ---------------------------------------------------- rcu_dynticks_nesting=0 (0000000000000000000000000000000000000000000000000000000000000000) State 364 file tiny.c line 97 function rcu_idle_enter thread 2 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 365 file fake.c line 110 function local_irq_restore thread 2 ---------------------------------------------------- local_irq_depth=0 (00000000000000000000000000000000) State 404 file tiny.c line 143 function rcu_idle_exit thread 1 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 405 file tiny.c line 144 function rcu_idle_exit thread 1 ---------------------------------------------------- oldval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 408 file tiny.c line 146 function rcu_idle_exit thread 1 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 411 file fake.c line 97 function local_irq_save thread 1 ---------------------------------------------------- local_irq_depth=1 (00000000000000000000000000000001) State 423 file tiny.c line 147 function rcu_idle_exit thread 1 ---------------------------------------------------- oldval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 434 file tiny.c line 152 function rcu_idle_exit thread 1 ---------------------------------------------------- rcu_dynticks_nesting=90071992547409920 (0000000101000000000000000000000000000000000000000000000000000000) State 437 file tiny.c line 153 function rcu_idle_exit thread 1 ---------------------------------------------------- oldval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 443 file tiny.c line 154 function rcu_idle_exit thread 1 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 444 file fake.c line 110 function local_irq_restore thread 1 ---------------------------------------------------- local_irq_depth=0 (00000000000000000000000000000000) State 458 file fake.c line 148 function thread_update thread 1 ---------------------------------------------------- x=1 (00000000000000000000000000000001) State 468 file tiny.c line 86 function rcu_idle_enter thread 1 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 469 file tiny.c line 87 function rcu_idle_enter thread 1 ---------------------------------------------------- newval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 472 file tiny.c line 89 function rcu_idle_enter thread 1 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 475 file fake.c line 97 function local_irq_save thread 1 ---------------------------------------------------- local_irq_depth=1 (00000000000000000000000000000001) State 494 file tiny.c line 93 function rcu_idle_enter thread 1 ---------------------------------------------------- newval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 498 file tiny.c line 96 function rcu_idle_enter thread 1 ---------------------------------------------------- newval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 503 file tiny.c line 222 function rcu_sched_qs thread 1 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 506 file tiny.c line 224 function rcu_sched_qs thread 1 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 509 file fake.c line 97 function local_irq_save thread 1 ---------------------------------------------------- local_irq_depth=2 (00000000000000000000000000000010) State 515 file tiny.c line 225 function rcu_sched_qs thread 1 ---------------------------------------------------- rcp=&rcu_sched_ctrlblk.rcucblist (0000001000000000000000000000000000000000000000000000000000000000) State 524 file tiny.c line 226 function rcu_sched_qs thread 1 ---------------------------------------------------- rcp=&rcu_bh_ctrlblk.rcucblist (0000001100000000000000000000000000000000000000000000000000000000) State 533 file tiny.c line 228 function rcu_sched_qs thread 1 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 534 file fake.c line 110 function local_irq_restore thread 1 ---------------------------------------------------- local_irq_depth=1 (00000000000000000000000000000001) State 538 file tiny.c line 77 function rcu_idle_enter_common thread 1 ---------------------------------------------------- rcu_dynticks_nesting=0 (0000000000000000000000000000000000000000000000000000000000000000) State 542 file tiny.c line 97 function rcu_idle_enter thread 1 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 543 file fake.c line 110 function local_irq_restore thread 1 ---------------------------------------------------- local_irq_depth=0 (00000000000000000000000000000000) State 582 file tiny.c line 143 function rcu_idle_exit thread 1 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 583 file tiny.c line 144 function rcu_idle_exit thread 1 ---------------------------------------------------- oldval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 586 file tiny.c line 146 function rcu_idle_exit thread 1 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 589 file fake.c line 97 function local_irq_save thread 1 ---------------------------------------------------- local_irq_depth=1 (00000000000000000000000000000001) State 601 file tiny.c line 147 function rcu_idle_exit thread 1 ---------------------------------------------------- oldval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 609 file tiny.c line 152 function rcu_idle_exit thread 1 ---------------------------------------------------- rcu_dynticks_nesting=90071992547409920 (0000000101000000000000000000000000000000000000000000000000000000) State 612 file tiny.c line 153 function rcu_idle_exit thread 1 ---------------------------------------------------- oldval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 618 file tiny.c line 154 function rcu_idle_exit thread 1 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 619 file fake.c line 110 function local_irq_restore thread 1 ---------------------------------------------------- local_irq_depth=0 (00000000000000000000000000000000) State 636 file fake.c line 152 function thread_update thread 1 ---------------------------------------------------- y=1 (00000000000000000000000000000001) State 641 file tiny.c line 86 function rcu_idle_enter thread 1 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 642 file tiny.c line 87 function rcu_idle_enter thread 1 ---------------------------------------------------- newval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 645 file tiny.c line 89 function rcu_idle_enter thread 1 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 648 file fake.c line 97 function local_irq_save thread 1 ---------------------------------------------------- local_irq_depth=1 (00000000000000000000000000000001) State 667 file tiny.c line 93 function rcu_idle_enter thread 1 ---------------------------------------------------- newval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 671 file tiny.c line 96 function rcu_idle_enter thread 1 ---------------------------------------------------- newval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 676 file tiny.c line 222 function rcu_sched_qs thread 1 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 679 file tiny.c line 224 function rcu_sched_qs thread 1 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 682 file fake.c line 97 function local_irq_save thread 1 ---------------------------------------------------- local_irq_depth=2 (00000000000000000000000000000010) State 688 file tiny.c line 225 function rcu_sched_qs thread 1 ---------------------------------------------------- rcp=&rcu_sched_ctrlblk.rcucblist (0000001000000000000000000000000000000000000000000000000000000000) State 697 file tiny.c line 226 function rcu_sched_qs thread 1 ---------------------------------------------------- rcp=&rcu_bh_ctrlblk.rcucblist (0000001100000000000000000000000000000000000000000000000000000000) State 706 file tiny.c line 228 function rcu_sched_qs thread 1 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 707 file fake.c line 110 function local_irq_restore thread 1 ---------------------------------------------------- local_irq_depth=1 (00000000000000000000000000000001) State 711 file tiny.c line 77 function rcu_idle_enter_common thread 1 ---------------------------------------------------- rcu_dynticks_nesting=0 (0000000000000000000000000000000000000000000000000000000000000000) State 715 file tiny.c line 97 function rcu_idle_enter thread 1 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 716 file fake.c line 110 function local_irq_restore thread 1 ---------------------------------------------------- local_irq_depth=0 (00000000000000000000000000000000) State 754 file tiny.c line 143 function rcu_idle_exit thread 2 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 755 file tiny.c line 144 function rcu_idle_exit thread 2 ---------------------------------------------------- oldval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 758 file tiny.c line 146 function rcu_idle_exit thread 2 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 761 file fake.c line 97 function local_irq_save thread 2 ---------------------------------------------------- local_irq_depth=1 (00000000000000000000000000000001) State 773 file tiny.c line 147 function rcu_idle_exit thread 2 ---------------------------------------------------- oldval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 781 file tiny.c line 152 function rcu_idle_exit thread 2 ---------------------------------------------------- rcu_dynticks_nesting=90071992547409920 (0000000101000000000000000000000000000000000000000000000000000000) State 784 file tiny.c line 153 function rcu_idle_exit thread 2 ---------------------------------------------------- oldval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 790 file tiny.c line 154 function rcu_idle_exit thread 2 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 791 file fake.c line 110 function local_irq_restore thread 2 ---------------------------------------------------- local_irq_depth=0 (00000000000000000000000000000000) State 810 file fake.c line 140 function rcu_reader thread 2 ---------------------------------------------------- __unbuffered_tpr_y=1 (00000000000000000000000000000001) State 820 file tiny.c line 86 function rcu_idle_enter thread 2 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 821 file tiny.c line 87 function rcu_idle_enter thread 2 ---------------------------------------------------- newval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 824 file tiny.c line 89 function rcu_idle_enter thread 2 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 827 file fake.c line 97 function local_irq_save thread 2 ---------------------------------------------------- local_irq_depth=1 (00000000000000000000000000000001) State 846 file tiny.c line 93 function rcu_idle_enter thread 2 ---------------------------------------------------- newval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 850 file tiny.c line 96 function rcu_idle_enter thread 2 ---------------------------------------------------- newval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 855 file tiny.c line 222 function rcu_sched_qs thread 2 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 858 file tiny.c line 224 function rcu_sched_qs thread 2 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 861 file fake.c line 97 function local_irq_save thread 2 ---------------------------------------------------- local_irq_depth=2 (00000000000000000000000000000010) State 867 file tiny.c line 225 function rcu_sched_qs thread 2 ---------------------------------------------------- rcp=&rcu_sched_ctrlblk.rcucblist (0000001000000000000000000000000000000000000000000000000000000000) State 876 file tiny.c line 226 function rcu_sched_qs thread 2 ---------------------------------------------------- rcp=&rcu_bh_ctrlblk.rcucblist (0000001100000000000000000000000000000000000000000000000000000000) State 885 file tiny.c line 228 function rcu_sched_qs thread 2 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 886 file fake.c line 110 function local_irq_restore thread 2 ---------------------------------------------------- local_irq_depth=1 (00000000000000000000000000000001) State 895 file -pthread_create line 20 function __actual_thread_spawn thread 2 ---------------------------------------------------- arg=NULL (0000000000000000000000000000000000000000000000000000000000000000) State 911 file tiny.c line 77 function rcu_idle_enter_common thread 2 ---------------------------------------------------- rcu_dynticks_nesting=0 (0000000000000000000000000000000000000000000000000000000000000000) State 915 file tiny.c line 97 function rcu_idle_enter thread 2 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 916 file fake.c line 110 function local_irq_restore thread 2 ---------------------------------------------------- local_irq_depth=0 (00000000000000000000000000000000) Violated property: file fake.c line 193 function main assertion __unbuffered_tpr_y == 0 || __unbuffered_tpr_x == 1 || ({ __sync_synchronize(); noassert; }) FALSE VERIFICATION FAILED real 0m19.006s user 0m18.781s sys 0m0.201s