bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-kernel--rcutorture.ko-ldv_main0_sequence_infinite_withcheck_stateful.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.: 278 182 1927 8703
Removed infinite loop in arch_local_irq_restore
Removed infinite loop in arch_local_save_flags
Removed infinite loop in arch_local_irq_disable
INFO: Compilation, preparation and instrumentation time: 0.334985971451
Removed calls to 'do_trace_rcu_torture_read' (function is undefined)
Removed calls to 'ftrace_dump' (function is undefined)
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 'call_rcu_sched' (function is undefined)
Removed calls to 'synchronize_sched' (function is undefined)
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_cpu_idle as symbolic
Defining function local_clock as symbolic
Removed calls to 'list_del' (function is undefined)
Removed calls to 'local_bh_disable' (function is undefined)
Removed calls to 'local_bh_enable' (function is undefined)
Removed calls to 'call_rcu_bh' (function is undefined)
Defining function rcu_batches_completed_bh as symbolic
Removed calls to 'synchronize_sched_expedited' (function is undefined)
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 '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 schedule_timeout_interruptible as symbolic
Defining function __srcu_read_lock as symbolic
Removed calls to 'synchronize_srcu_expedited' (function is undefined)
Removed calls to 'trace_hardirqs_off' (function is undefined)
Removed calls to 'trace_hardirqs_on' (function is undefined)
Removed calls to 'kthread_bind' (function is undefined)
Removed calls to 'mutex_lock' (function is undefined)
Defining function printk as symbolic
Removed calls to 'mutex_unlock' (function is undefined)
Defining function kthread_stop as symbolic
Defining function __cpu_to_node as symbolic
Removed calls to 'init_rcu_head_on_stack' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'destroy_rcu_head_on_stack' (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_uninterruptible as symbolic
Defining function kthread_should_stop as symbolic
Defining function _cond_resched as symbolic
Defining function mutex_trylock as symbolic
Defining function round_jiffies_relative as symbolic
Removed calls to 'ldv_handler_precall' (function is undefined)
Removed calls to 'free_cpumask_var' (function is undefined)
Removed calls to 'rcutorture_record_test_transition' (function is undefined)
Removed calls to 'unregister_cpu_notifier' (function is undefined)
Defining function unregister_reboot_notifier as symbolic
Removed calls to 'set_user_nice' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to 'rcutorture_record_progress' (function is undefined)
Removed calls to 'init_timer_on_stack_key' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Defining function alloc_cpumask_var as symbolic
Removed calls to 'get_online_cpus' (function is undefined)
Removed calls to 'put_online_cpus' (function is undefined)
Defining function register_cpu_notifier as symbolic
Defining function register_reboot_notifier as symbolic
Defining function set_cpus_allowed_ptr as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function mod_timer as symbolic
Defining function rcu_read_lock_bh_held as symbolic
Defining function del_timer_sync as symbolic
Defining function rcu_lockdep_current_cpu_online as symbolic
Defining function lock_is_held as symbolic
Defining function __bitmap_weight as symbolic
Linked our definitions to these undefined functions:
  strcmp
  __kmalloc
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 0.276430130005
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 229 160 776 3558
INFO: Starting verification
KLEE: WARNING ONCE: function "rcutorture_trace_dump" 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_sync_torture_deferred_free" 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 "arch_local_irq_save" has inline asm
KLEE: WARNING ONCE: function "arch_local_irq_restore" has inline asm
KLEE: WARNING ONCE: function "arch_local_save_flags" 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_boost" has inline asm
KLEE: WARNING ONCE: function "rcu_torture_barrier_cbf" 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_fakewriter" has inline asm
KLEE: WARNING ONCE: function "rcu_torture_reader" has inline asm
KLEE: WARNING ONCE: function "rcu_torture_shuffle" has inline asm
KLEE: WARNING ONCE: function "rcu_torture_stats_print" has inline asm
KLEE: WARNING ONCE: function "rcu_torture_timer" has inline asm
KLEE: WARNING ONCE: function "rcu_read_lock_sched_held" 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: 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: ERROR: /tmp/symbiotic-JvWkRw/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-kernel--rcutorture.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:6919: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: WARNING ONCE: calling external: rcu_barrier() at /tmp/symbiotic-JvWkRw/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-kernel--rcutorture.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:6728
KLEE: ERROR: /tmp/symbiotic-JvWkRw/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-kernel--rcutorture.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:6727: failed external call: rcu_barrier
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: ERROR: concretized symbolic size to 2^17,analysis may be unsound
KLEE: output directory is "/tmp/symbiotic-JvWkRw/klee-out-0"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: function "rcutorture_trace_dump" 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_sync_torture_deferred_free" 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 "arch_local_irq_save" has inline asm
KLEE: WARNING ONCE: function "arch_local_irq_restore" has inline asm
KLEE: WARNING ONCE: function "arch_local_save_flags" 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_boost" has inline asm
KLEE: WARNING ONCE: function "rcu_torture_barrier_cbf" 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_fakewriter" has inline asm
KLEE: WARNING ONCE: function "rcu_torture_reader" has inline asm
KLEE: WARNING ONCE: function "rcu_torture_shuffle" has inline asm
KLEE: WARNING ONCE: function "rcu_torture_stats_print" has inline asm
KLEE: WARNING ONCE: function "rcu_torture_timer" has inline asm
KLEE: WARNING ONCE: function "rcu_read_lock_sched_held" 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: 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: ERROR: /tmp/symbiotic-JvWkRw/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-kernel--rcutorture.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:6919: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: WARNING ONCE: calling external: rcu_barrier() at /tmp/symbiotic-JvWkRw/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-kernel--rcutorture.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:6728
KLEE: ERROR: /tmp/symbiotic-JvWkRw/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-kernel--rcutorture.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:6727: failed external call: rcu_barrier
KLEE: NOTE: now ignoring this error at this location
KLEE: NOTE: found huge malloc, returning 0
KLEE: WARNING ONCE: ERROR: concretized symbolic size to 2^17,analysis may be unsound
0  klee            0x00000000012fcca8 llvm::sys::PrintStackTrace(llvm::raw_ostream&) + 56
1  klee            0x00000000012fac7e llvm::sys::RunSignalHandlers() + 62
2  klee            0x00000000012fadcc
3  libpthread.so.0 0x00007f7ba9beb390
4  klee            0x00000000005d20ab klee::Executor::executeMemoryOperation(klee::ExecutionState&, bool, klee::ref<klee::Expr>, klee::ref<klee::Expr>, klee::KInstruction*) + 75
5  klee            0x00000000005d560d klee::Executor::executeInstruction(klee::ExecutionState&, klee::KInstruction*) + 2285
6  klee            0x00000000005da8c5 klee::Executor::run(klee::ExecutionState&) + 2117
7  klee            0x00000000005daeef klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1391
8  klee            0x0000000000593c63 main + 8867
9  libc.so.6       0x00007f7ba8f8f830 __libc_start_main + 240
10 klee            0x00000000005bed49 _start + 41
Running the verifier failed
RESULT: unknown
INFO: Total time elapsed: 0.721617937088
