bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--md--raid456.ko_false-unreach-call.cil.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.: 257 778 6851 41229
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_linux_kernel_module_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 1.27353000641
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Removed calls to 'kmem_cache_free' (function is undefined)
Defining function md_allow_write as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'put_page' (function is undefined)
Removed calls to 'md_wakeup_thread' (function is undefined)
Removed calls to 'trace_hardirqs_off' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'trace_hardirqs_on' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to '__ldv_linux_kernel_locking_spinlock_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Defining function __cpu_to_node as symbolic
Defining function queue_work_on as symbolic
Defining function __ldv_linux_kernel_locking_spinlock_atomic_dec_and_lock as symbolic
Defining function llist_add_batch as symbolic
Defining function external_allocated_data as symbolic
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to 'md_flush_request' (function is undefined)
Removed calls to 'md_write_start' (function is undefined)
Removed calls to 'lockdep_rcu_suspicious' (function is undefined)
Removed calls to 'blk_recount_segments' (function is undefined)
Removed calls to 'bio_put' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to 'generic_make_request' (function is undefined)
Removed calls to 'prepare_to_wait' (function is undefined)
Removed calls to 'md_write_end' (function is undefined)
Removed calls to 'bio_endio' (function is undefined)
Removed calls to 'flush_signals' (function is undefined)
Removed calls to 'md_set_array_sectors' (function is undefined)
Removed calls to 'blk_queue_io_min' (function is undefined)
Removed calls to 'blk_queue_io_opt' (function is undefined)
Removed calls to 'blk_queue_max_write_same_sectors' (function is undefined)
Removed calls to 'disk_stack_limits' (function is undefined)
Removed calls to 'md_unregister_thread' (function is undefined)
Removed calls to 'kernfs_notify' (function is undefined)
Removed calls to 'bitmap_end_sync' (function is undefined)
Removed calls to 'bitmap_close_sync' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'sysfs_notify' (function is undefined)
Removed calls to 'bitmap_cond_end_sync' (function is undefined)
Removed calls to 'lock_acquire' (function is undefined)
Removed calls to 'lock_release' (function is undefined)
Removed calls to 'mddev_suspend' (function is undefined)
Removed calls to 'mddev_resume' (function is undefined)
Removed calls to 'md_new_event' (function is undefined)
Removed calls to 'ldv_after_alloc' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'get_online_cpus' (function is undefined)
Removed calls to 'put_online_cpus' (function is undefined)
Defining function printk as symbolic
Removed calls to '__init_work' (function is undefined)
Defining function bdevname as symbolic
Defining function sprintf as symbolic
Removed calls to 'md_check_recovery' (function is undefined)
Removed calls to 'blk_start_plug' (function is undefined)
Removed calls to 'bitmap_unplug' (function is undefined)
Removed calls to 'dma_issue_pending_all' (function is undefined)
Removed calls to 'blk_finish_plug' (function is undefined)
Removed calls to 'kmem_cache_destroy' (function is undefined)
Removed calls to 'unregister_cpu_notifier' (function is undefined)
Removed calls to 'free_percpu' (function is undefined)
Defining function md_register_thread as symbolic
Removed calls to 'mddev_unlock' (function is undefined)
Defining function kstrtoull as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to 'flush_workqueue' (function is undefined)
Removed calls to '___might_sleep' (function is undefined)
Removed calls to 'md_error' (function is undefined)
Removed calls to 'bitmap_endwrite' (function is undefined)
Removed calls to 'md_done_sync' (function is undefined)
Removed calls to '__trace_note_message' (function is undefined)
Removed calls to 'async_tx_quiesce' (function is undefined)
Removed calls to 'md_wait_for_blocked_rdev' (function is undefined)
Defining function _cond_resched as symbolic
Removed calls to 'bio_init' (function is undefined)
Defining function rdev_set_badblocks as symbolic
Defining function debug_lockdep_rcu_enabled as symbolic
Defining function rcu_is_watching as symbolic
Defining function rcu_lockdep_current_cpu_online as symbolic
Defining function lock_is_held as symbolic
Defining function rcu_read_lock_held as symbolic
Defining function md_is_badblock as symbolic
Defining function async_syndrome_val as symbolic
Defining function async_xor_val as symbolic
Defining function async_trigger_callback as symbolic
Defining function async_gen_syndrome as symbolic
Defining function async_memcpy as symbolic
Defining function async_xor as symbolic
Defining function async_raid6_datap_recov as symbolic
Defining function async_raid6_2data_recov as symbolic
Defining function prepare_to_wait_event as symbolic
Defining function bitmap_startwrite as symbolic
Defining function llist_reverse_order as symbolic
Defining function kmem_cache_create as symbolic
Defining function __alloc_percpu as symbolic
Defining function register_cpu_notifier as symbolic
Defining function __bitmap_weight as symbolic
Defining function revalidate_disk as symbolic
Defining function sysfs_create_link as symbolic
Removed calls to 'list_del' (function is undefined)
Defining function bitmap_resize as symbolic
Defining function bitmap_start_sync as symbolic
Defining function schedule_timeout_uninterruptible as symbolic
Defining function seq_printf as symbolic
Defining function autoremove_wake_function as symbolic
Defining function blk_check_plugged as symbolic
Defining function bio_clone_mddev as symbolic
Removed calls to 'destroy_workqueue' (function is undefined)
Defining function unregister_md_personality as symbolic
Defining function __alloc_workqueue_key as symbolic
Defining function register_md_personality as symbolic
Removed calls to 'ldv_assert' (function is undefined)
Linked our definitions to these undefined functions:
  __memset
  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: 1.45142793655
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 387 614 3644 21208
INFO: Starting verification
WARNING: this target does not support the llvm.returnaddress intrinsic.
WARNING: this target does not support the llvm.returnaddress intrinsic.
KLEE: WARNING ONCE: function "drop_one_stripe" has inline asm
KLEE: WARNING ONCE: function "release_stripe" has inline asm
KLEE: WARNING ONCE: function "arch_local_irq_save" has inline asm
KLEE: WARNING ONCE: function "do_release_stripe" has inline asm
KLEE: WARNING ONCE: function "raid5_wakeup_stripe_thread" has inline asm
KLEE: WARNING ONCE: function "get_free_stripe" has inline asm
KLEE: WARNING ONCE: function "make_request" has inline asm
KLEE: WARNING ONCE: function "run" has inline asm
KLEE: WARNING ONCE: function "error" has inline asm
KLEE: WARNING ONCE: function "raid5_add_disk" has inline asm
KLEE: WARNING ONCE: function "raid5_remove_disk" has inline asm
KLEE: WARNING ONCE: function "raid5_spare_active" has inline asm
KLEE: WARNING ONCE: function "sync_request" has inline asm
KLEE: WARNING ONCE: function "raid5_resize" has inline asm
KLEE: WARNING ONCE: function "raid5_start_reshape" has inline asm
KLEE: WARNING ONCE: function "raid5_finish_reshape" has inline asm
KLEE: WARNING ONCE: function "setup_conf" has inline asm
KLEE: WARNING ONCE: function "raid456_cpu_notify" has inline asm
KLEE: WARNING ONCE: function "raid5d" has inline asm
KLEE: WARNING ONCE: function "free_conf" has inline asm
KLEE: WARNING ONCE: function "release_stripe_list" has inline asm
KLEE: WARNING ONCE: function "handle_active_stripes" has inline asm
KLEE: WARNING ONCE: function "handle_stripe" has inline asm
KLEE: WARNING ONCE: function "rdev_dec_pending" has inline asm
KLEE: WARNING ONCE: function "handle_stripe_clean_event" has inline asm
KLEE: WARNING ONCE: function "schedule_reconstruction" has inline asm
KLEE: WARNING ONCE: function "get_active_stripe" has inline asm
KLEE: WARNING ONCE: function "compute_blocknr" has inline asm
KLEE: WARNING ONCE: function "raid5_compute_sector" has inline asm
KLEE: WARNING ONCE: function "ops_complete_biofill" has inline asm
KLEE: WARNING ONCE: function "ops_complete_compute" has inline asm
KLEE: WARNING ONCE: function "ops_complete_reconstruct" has inline asm
KLEE: WARNING ONCE: function "ops_complete_check" has inline asm
KLEE: WARNING ONCE: function "trace_block_bio_complete" has inline asm
KLEE: WARNING ONCE: function "rcu_read_lock_sched_held" has inline asm
KLEE: WARNING ONCE: function "mark_target_uptodate" has inline asm
KLEE: WARNING ONCE: function "read_seqcount_begin" has inline asm
KLEE: WARNING ONCE: function "add_stripe_bio" has inline asm
KLEE: WARNING ONCE: function "lock_all_device_hash_locks_irq" has inline asm
KLEE: WARNING ONCE: function "unlock_all_device_hash_locks_irq" has inline asm
KLEE: WARNING ONCE: function "check_reshape" has inline asm
KLEE: WARNING ONCE: function "raid5_unplug" has inline asm
KLEE: WARNING ONCE: function "raid5_check_reshape" has inline asm
KLEE: WARNING: undefined reference to function: ldv_after_alloc
KLEE: WARNING: undefined reference to function: md_do_sync
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_70be421c-e669-446b-a90c-6795188b5c22/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
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: flushing 65536 bytes on read, may be slow and/or crash: MO93[65536] allocated at global:__per_cpu_offset
KLEE: ERROR: /tmp/symbiotic-25FfAj/linux-4.0-rc1---drivers--md--raid456.ko_false-unreach-call.cil.c:21644: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-25FfAj/linux-4.0-rc1---drivers--md--raid456.ko_false-unreach-call.cil.c:21649: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-25FfAj/linux-4.0-rc1---drivers--md--raid456.ko_false-unreach-call.cil.c:21753: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-25FfAj/linux-4.0-rc1---drivers--md--raid456.ko_false-unreach-call.cil.c:21765: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-25FfAj/linux-4.0-rc1---drivers--md--raid456.ko_false-unreach-call.cil.c:21640: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-25FfAj/linux-4.0-rc1---drivers--md--raid456.ko_false-unreach-call.cil.c:21777: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-25FfAj/linux-4.0-rc1---drivers--md--raid456.ko_false-unreach-call.cil.c:21789: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-25FfAj/linux-4.0-rc1---drivers--md--raid456.ko_false-unreach-call.cil.c:21685: divide by zero
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-25FfAj/linux-4.0-rc1---drivers--md--raid456.ko_false-unreach-call.cil.c:21815: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-25FfAj/linux-4.0-rc1---drivers--md--raid456.ko_false-unreach-call.cil.c:21815: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-25FfAj/linux-4.0-rc1---drivers--md--raid456.ko_false-unreach-call.cil.c:21816: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-25FfAj/linux-4.0-rc1---drivers--md--raid456.ko_false-unreach-call.cil.c:21699: divide by zero
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-25FfAj/linux-4.0-rc1---drivers--md--raid456.ko_false-unreach-call.cil.c:21649: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
