bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-kernel--rcu--rcutorture.ko-entry_point_true-unreach-call.cil.out.c


--------------------------------------------------------------------------------


5.0.0-KLEE:86e6f6f8-dg:03407af1-symbiotic:a8aa8ad6-minisat:3db58943-stp:17249213-sbt-instrumentation:dd7e4312
INFO: After compilation stats: Globals/Functions/Blocks/Instr.: 236 141 1971 8060
Removed infinite loop in ldv_stop
Removed infinite loop in arch_local_save_flags
Removed infinite loop in arch_local_irq_disable
Removed infinite loop in arch_local_irq_enable
INFO: Compilation, preparation and instrumentation time: 0.336654901505
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'kthread_bind' (function is undefined)
Removed calls to '_torture_stop_kthread' (function is undefined)
Defining function printk as symbolic
Defining function __cpu_to_node as symbolic
Removed calls to 'init_rcu_head_on_stack' (function is undefined)
Removed calls to 'stutter_wait' (function is undefined)
Removed calls to 'call_rcu_sched' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'torture_shutdown_absorb' (function is undefined)
Removed calls to 'destroy_rcu_head_on_stack' (function is undefined)
Removed calls to 'torture_kthread_stopping' (function is undefined)
Defining function kthread_create_on_node as symbolic
Defining function wake_up_process as symbolic
Defining function sched_setscheduler as symbolic
Defining function schedule_timeout_interruptible as symbolic
Defining function torture_must_stop as symbolic
Defining function _cond_resched as symbolic
Defining function mutex_trylock as symbolic
Defining function schedule_timeout_uninterruptible as symbolic
Defining function kthread_should_stop as symbolic
Removed calls to 'lock_acquire' (function is undefined)
Removed calls to 'lockdep_rcu_suspicious' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Removed calls to '__udelay' (function is undefined)
Removed calls to 'lock_release' (function is undefined)
Removed calls to 'synchronize_sched' (function is undefined)
Defining function get_state_synchronize_rcu as symbolic
Defining function torture_must_stop_irq as symbolic
Removed calls to '_raw_spin_lock_bh' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to '_raw_spin_unlock_bh' (function is undefined)
Defining function rcu_batches_completed as symbolic
Defining function debug_lockdep_rcu_enabled as symbolic
Defining function rcu_is_watching as symbolic
Defining function torture_random as symbolic
Removed calls to '__local_bh_disable_ip' (function is undefined)
Removed calls to '__local_bh_enable_ip' (function is undefined)
Removed calls to 'call_rcu_bh' (function is undefined)
Removed calls to 'synchronize_sched_expedited' (function is undefined)
Defining function rcu_batches_completed_bh as symbolic
Removed calls to '__srcu_read_unlock' (function is undefined)
Removed calls to 'call_srcu' (function is undefined)
Removed calls to 'synchronize_srcu' (function is undefined)
Removed calls to 'synchronize_srcu_expedited' (function is undefined)
Removed calls to 'srcu_barrier' (function is undefined)
Defining function sprintf as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function find_next_bit as symbolic
Defining function srcu_batches_completed as symbolic
Defining function __srcu_read_lock as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'do_trace_rcu_torture_read' (function is undefined)
Removed calls to 'ftrace_dump' (function is undefined)
Defining function rcu_read_lock_bh_held as symbolic
Defining function lock_is_held as symbolic
Defining function rcu_lockdep_current_cpu_online as symbolic
Defining function trace_clock_local as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'rcu_sched_force_quiescent_state' (function is undefined)
Removed calls to 'rcu_barrier_sched' (function is undefined)
Removed calls to 'rcu_bh_force_quiescent_state' (function is undefined)
Removed calls to 'rcu_barrier_bh' (function is undefined)
Removed calls to 'synchronize_rcu_bh' (function is undefined)
Removed calls to 'rcu_force_quiescent_state' (function is undefined)
Removed calls to 'cond_synchronize_rcu' (function is undefined)
Removed calls to 'synchronize_rcu_expedited' (function is undefined)
Removed calls to 'rcu_barrier' (function is undefined)
Removed calls to 'torture_init_end' (function is undefined)
Removed calls to 'process_srcu' (function is undefined)
Removed calls to 'delayed_work_timer_fn' (function is undefined)
Removed calls to 'ldv_check_final_state' (function is undefined)
Defining function ldv_setup_6 as symbolic
Defining function ldv_release_6 as symbolic
Defining function ldv_setup_3 as symbolic
Defining function ldv_release_3 as symbolic
Defining function ldv_setup_7 as symbolic
Defining function ldv_release_7 as symbolic
Defining function ldv_setup_8 as symbolic
Defining function ldv_release_8 as symbolic
Defining function ldv_setup_4 as symbolic
Defining function ldv_release_4 as symbolic
Removed calls to 'rcutorture_record_test_transition' (function is undefined)
Removed calls to 'unregister_cpu_notifier' (function is undefined)
Defining function torture_init_begin as symbolic
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to 'rcutorture_record_progress' (function is undefined)
Defining function _torture_create_kthread as symbolic
Defining function del_timer_sync as symbolic
Defining function mod_timer as symbolic
Removed calls to 'list_del' (function is undefined)
Defining function __bitmap_weight as symbolic
Defining function torture_cleanup as symbolic
Defining function torture_onoff_failures as symbolic
Defining function kmem_cache_alloc as symbolic
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  strcmp
  __kmalloc
  kfree
  __VERIFIER_assume
  __VERIFIER_calloc0
  __VERIFIER_error
  __VERIFIER_exit
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
  __VERIFIER_nondet_pointer_named
  __VERIFIER_nondet_ulong_named
INFO: After-slicing optimizations and preparation time: 0.292808055878
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 211 123 645 2694
INFO: Starting verification
KLEE: WARNING ONCE: function "rcu_torture_boost" has inline asm
KLEE: WARNING ONCE: function "rcu_torture_read_lock" has inline asm
KLEE: WARNING ONCE: function "rcu_torture_read_unlock" has inline asm
KLEE: WARNING ONCE: function "rcu_torture_cb" has inline asm
KLEE: WARNING ONCE: function "rcu_torture_free" has inline asm
KLEE: WARNING ONCE: function "srcu_torture_stats" has inline asm
KLEE: WARNING ONCE: function "sched_torture_read_lock" has inline asm
KLEE: WARNING ONCE: function "sched_torture_read_unlock" has inline asm
KLEE: WARNING ONCE: function "rcu_torture_timer" has inline asm
KLEE: WARNING ONCE: function "main" has inline asm
KLEE: WARNING ONCE: function "rcu_torture_writer" has inline asm
KLEE: WARNING ONCE: function "rcu_torture_pipe_update" has inline asm
KLEE: WARNING: undefined reference to variable: boot_tvec_bases
KLEE: WARNING: undefined reference to function: call_rcu_bh
KLEE: WARNING: undefined reference to function: call_rcu_sched
KLEE: WARNING: undefined reference to function: cond_synchronize_rcu
KLEE: WARNING: undefined reference to function: delayed_work_timer_fn
KLEE: WARNING: undefined reference to function: process_srcu
KLEE: WARNING: undefined reference to function: rcu_barrier
KLEE: WARNING: undefined reference to function: rcu_barrier_bh
KLEE: WARNING: undefined reference to function: rcu_barrier_sched
KLEE: WARNING: undefined reference to function: rcu_bh_force_quiescent_state
KLEE: WARNING: undefined reference to function: rcu_force_quiescent_state
KLEE: WARNING: undefined reference to function: rcu_sched_force_quiescent_state
KLEE: WARNING: undefined reference to function: synchronize_rcu_bh
KLEE: WARNING: undefined reference to function: synchronize_rcu_expedited
KLEE: WARNING: undefined reference to function: synchronize_sched
KLEE: WARNING: undefined reference to function: synchronize_sched_expedited
KLEE: WARNING: Type for boot_tvec_bases is not sized
KLEE: WARNING: Unable to find size for global variable: boot_tvec_bases (use will result in out of bounds access)
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_4fc5a43e-1f8a-4ac8-b289-f74bb0d7bcfb/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 5952 states (over memory cap)
KLEE: WARNING: killing 6181 states (over memory cap)
KLEE: WARNING: killing 6692 states (over memory cap)
KLEE: WARNING: killing 6877 states (over memory cap)
KLEE: WARNING: killing 7673 states (over memory cap)
KLEE: WARNING: killing 7907 states (over memory cap)
KLEE: WARNING: killing 7630 states (over memory cap)
KLEE: WARNING: killing 7915 states (over memory cap)
KLEE: WARNING: killing 8714 states (over memory cap)
KLEE: WARNING: killing 8816 states (over memory cap)
KLEE: WARNING: killing 9154 states (over memory cap)
KLEE: WARNING: killing 4947 states (over memory cap)
KLEE: WARNING: killing 5043 states (over memory cap)
KLEE: WARNING: killing 5046 states (over memory cap)
KLEE: WARNING: killing 9084 states (over memory cap)
KLEE: WARNING: killing 4958 states (over memory cap)
KLEE: WARNING: killing 5053 states (over memory cap)
KLEE: WARNING: killing 5057 states (over memory cap)
KLEE: WARNING: killing 5391 states (over memory cap)
KLEE: WARNING: killing 5206 states (over memory cap)
KLEE: WARNING: killing 5443 states (over memory cap)
KLEE: WARNING: killing 5967 states (over memory cap)
KLEE: WARNING: killing 5923 states (over memory cap)
KLEE: WARNING: killing 5550 states (over memory cap)
KLEE: WARNING: killing 5598 states (over memory cap)
KLEE: WARNING: killing 5836 states (over memory cap)
KLEE: WARNING: killing 5978 states (over memory cap)
KLEE: WARNING: killing 5982 states (over memory cap)
KLEE: WARNING: killing 6316 states (over memory cap)
KLEE: WARNING: killing 6412 states (over memory cap)
KLEE: WARNING: killing 6558 states (over memory cap)
KLEE: WARNING: killing 6703 states (over memory cap)
KLEE: WARNING: killing 6659 states (over memory cap)
KLEE: WARNING: killing 7231 states (over memory cap)
KLEE: WARNING: killing 7470 states (over memory cap)
KLEE: WARNING: killing 7234 states (over memory cap)
KLEE: WARNING: killing 7711 states (over memory cap)
KLEE: WARNING: killing 7999 states (over memory cap)
KLEE: WARNING: killing 8051 states (over memory cap)
KLEE: WARNING: killing 8383 states (over memory cap)
KLEE: WARNING: killing 8626 states (over memory cap)
KLEE: WARNING: killing 8959 states (over memory cap)
KLEE: WARNING: killing 9580 states (over memory cap)
KLEE: WARNING: killing 9583 states (over memory cap)
KLEE: WARNING: killing 9439 states (over memory cap)
KLEE: WARNING: killing 9962 states (over memory cap)
KLEE: WARNING: killing 10867 states (over memory cap)
KLEE: WARNING: killing 10485 states (over memory cap)
KLEE: WARNING: killing 11152 states (over memory cap)
KLEE: WARNING: killing 11099 states (over memory cap)
KLEE: WARNING: killing 11096 states (over memory cap)
KLEE: WARNING: killing 11470 states (over memory cap)
KLEE: WARNING: killing 12464 states (over memory cap)
KLEE: WARNING: killing 11793 states (over memory cap)
KLEE: WARNING: killing 11546 states (over memory cap)
KLEE: WARNING: killing 12393 states (over memory cap)
KLEE: WARNING: killing 12051 states (over memory cap)
KLEE: WARNING: killing 13045 states (over memory cap)
KLEE: WARNING: killing 12604 states (over memory cap)
KLEE: WARNING: killing 12927 states (over memory cap)
KLEE: WARNING: killing 13540 states (over memory cap)
KLEE: WARNING: killing 13241 states (over memory cap)
KLEE: WARNING: killing 13191 states (over memory cap)
KLEE: WARNING: killing 13227 states (over memory cap)
KLEE: WARNING: killing 12882 states (over memory cap)
KLEE: WARNING: killing 12589 states (over memory cap)
KLEE: WARNING: killing 12810 states (over memory cap)
KLEE: WARNING: killing 13367 states (over memory cap)
KLEE: WARNING: killing 13399 states (over memory cap)
KLEE: WARNING: killing 13576 states (over memory cap)
KLEE: WARNING: killing 13374 states (over memory cap)
KLEE: WARNING: killing 13315 states (over memory cap)
KLEE: WARNING: killing 13120 states (over memory cap)
KLEE: WARNING: killing 13057 states (over memory cap)
KLEE: WARNING: killing 13561 states (over memory cap)
KLEE: WARNING: killing 13224 states (over memory cap)
KLEE: WARNING: killing 13206 states (over memory cap)
KLEE: WARNING: killing 13854 states (over memory cap)
KLEE: WARNING: killing 13138 states (over memory cap)
KLEE: WARNING: killing 12939 states (over memory cap)
KLEE: WARNING: killing 13251 states (over memory cap)
KLEE: WARNING: killing 13289 states (over memory cap)
KLEE: WARNING: killing 13184 states (over memory cap)
KLEE: WARNING: killing 13588 states (over memory cap)
KLEE: WARNING: killing 13438 states (over memory cap)
KLEE: WARNING: killing 13143 states (over memory cap)
KLEE: WARNING: killing 12986 states (over memory cap)
KLEE: WARNING: killing 13957 states (over memory cap)
KLEE: WARNING: killing 13573 states (over memory cap)
KLEE: WARNING: killing 13468 states (over memory cap)
KLEE: WARNING: killing 13320 states (over memory cap)
KLEE: WARNING: killing 13394 states (over memory cap)
KLEE: WARNING: killing 13199 states (over memory cap)
KLEE: WARNING: killing 13420 states (over memory cap)
KLEE: WARNING: killing 13035 states (over memory cap)
KLEE: WARNING: killing 13113 states (over memory cap)
KLEE: WARNING: killing 13468 states (over memory cap)
KLEE: WARNING: killing 13458 states (over memory cap)
KLEE: WARNING: killing 13352 states (over memory cap)
KLEE: WARNING: killing 13800 states (over memory cap)
KLEE: WARNING: killing 13557 states (over memory cap)
KLEE: WARNING: killing 13728 states (over memory cap)
KLEE: WARNING: killing 12709 states (over memory cap)
KLEE: WARNING: killing 13888 states (over memory cap)
KLEE: WARNING: killing 13461 states (over memory cap)
KLEE: WARNING: killing 13859 states (over memory cap)
KLEE: WARNING: killing 14079 states (over memory cap)
KLEE: WARNING: killing 13288 states (over memory cap)
KLEE: WARNING: killing 13093 states (over memory cap)
KLEE: WARNING: killing 13399 states (over memory cap)
KLEE: WARNING: killing 12973 states (over memory cap)
KLEE: WARNING: killing 12961 states (over memory cap)
KLEE: WARNING: killing 13905 states (over memory cap)
KLEE: WARNING: killing 13346 states (over memory cap)
KLEE: WARNING: killing 13696 states (over memory cap)
KLEE: WARNING: killing 13051 states (over memory cap)
KLEE: WARNING: killing 13583 states (over memory cap)
KLEE: WARNING: killing 13481 states (over memory cap)
KLEE: WARNING: killing 12970 states (over memory cap)
KLEE: WARNING: killing 13136 states (over memory cap)
KLEE: WARNING: killing 13764 states (over memory cap)
KLEE: WARNING: killing 13476 states (over memory cap)
KLEE: WARNING: killing 13734 states (over memory cap)
KLEE: WARNING: killing 12778 states (over memory cap)
