bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-32_7a-drivers--md--md-mod.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.: 746 699 8435 48644
Removed infinite loop in mddev_suspend
Removed infinite loop in write_page
Removed infinite loop in sync_super
Removed infinite loop in bitmap_create
Removed infinite loop in free_buffers
Removed infinite loop in bitmap_new_disk_sb
Removed infinite loop in get_page
Removed infinite loop in md_write_start
Removed infinite loop in arch_local_irq_restore
Removed infinite loop in arch_local_save_flags
Removed infinite loop in arch_local_irq_disable
Removed infinite loop in md_open
Removed infinite loop in md_release
Removed infinite loop in md_ioctl
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 1.63815593719
Defining function bio_alloc_bioset as symbolic
Defining function bio_clone_bioset as symbolic
Removed calls to '__wake_up' (function is undefined)
Removed calls to 'synchronize_sched' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Defining function prepare_to_wait_event as symbolic
Defining function del_timer_sync as symbolic
Removed calls to 'lock_acquire' (function is undefined)
Removed calls to 'lockdep_rcu_suspicious' (function is undefined)
Removed calls to 'lock_release' (function is undefined)
Defining function debug_lockdep_rcu_enabled as symbolic
Defining function rcu_is_watching as symbolic
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to 'submit_bio' (function is undefined)
Defining function queue_work_on as symbolic
Removed calls to 'bio_endio' (function is undefined)
Removed calls to 'bio_put' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'sysfs_remove_group' (function is undefined)
Removed calls to 'kernfs_put' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'put_page' (function is undefined)
Defining function bio_add_page as symbolic
Defining function submit_bio_wait as symbolic
Defining function printk as symbolic
Defining function blk_integrity_compare as symbolic
Defining function blk_integrity_register as symbolic
Defining function bioset_integrity_create as symbolic
Removed calls to 'blk_integrity_unregister' (function is undefined)
Removed calls to 'bd_unlink_disk_holder' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to 'sysfs_remove_link' (function is undefined)
Removed calls to 'blkdev_put' (function is undefined)
Removed calls to 'kobject_put' (function is undefined)
Defining function bdevname as symbolic
Removed calls to 'kobject_del' (function is undefined)
Defining function kobject_get as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'sysfs_notify' (function is undefined)
Removed calls to 'kernfs_notify' (function is undefined)
Defining function get_seconds as symbolic
Defining function submit_bh as symbolic
Defining function file_path as symbolic
Removed calls to 'invalidate_bdev' (function is undefined)
Removed calls to 'module_put' (function is undefined)
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Removed calls to 'blk_queue_merge_bvec' (function is undefined)
Defining function __request_module as symbolic
Defining function sync_blockdev as symbolic
Defining function bioset_create as symbolic
Defining function try_module_get as symbolic
Defining function strlcpy as symbolic
Removed calls to 'blk_sync_queue' (function is undefined)
Defining function sysfs_create_group as symbolic
Defining function sprintf as symbolic
Defining function sysfs_create_link as symbolic
Defining function kernfs_find_and_get_ns as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'fput' (function is undefined)
Removed calls to 'free_buffer_head' (function is undefined)
Defining function invalidate_mapping_pages as symbolic
Defining function kthread_stop as symbolic
Defining function vfs_fsync as symbolic
Defining function alloc_pages_current as symbolic
Removed calls to 'dump_page' (function is undefined)
Defining function alloc_page_buffers as symbolic
Defining function bmap as symbolic
Defining function __get_page_tail as symbolic
Removed calls to 'flush_workqueue' (function is undefined)
Removed calls to 'bioset_free' (function is undefined)
Removed calls to 'kernel_sigaction' (function is undefined)
Removed calls to 'flush_signals' (function is undefined)
Defining function kthread_create_on_node as symbolic
Defining function wake_up_process as symbolic
Defining function kthread_should_stop as symbolic
Defining function schedule_timeout as symbolic
Removed calls to '__list_add' (function is undefined)
Defining function mod_timer as symbolic
Removed calls to 'prepare_to_wait' (function is undefined)
Removed calls to 'blk_start_plug' (function is undefined)
Removed calls to '___might_sleep' (function is undefined)
Removed calls to 'msleep' (function is undefined)
Removed calls to 'blk_finish_plug' (function is undefined)
Defining function autoremove_wake_function as symbolic
Defining function _cond_resched as symbolic
Defining function find_next_bit as symbolic
Defining function _atomic_dec_and_lock as symbolic
Defining function mutex_trylock as symbolic
Defining function __msecs_to_jiffies as symbolic
Removed calls to 'trace_hardirqs_off' (function is undefined)
Removed calls to 'trace_hardirqs_on' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function __memmove as symbolic
Defining function _raw_spin_lock_irqsave as symbolic
Defining function mutex_lock_interruptible as symbolic
Defining function kstrtouint as symbolic
Defining function kstrtoll as symbolic
Defining function kstrtoull as symbolic
Defining function simple_strtoul as symbolic
Defining function skip_spaces as symbolic
Defining function seq_printf as symbolic
Defining function seq_file_path as symbolic
Defining function capable as symbolic
Defining function sscanf as symbolic
Defining function snprintf as symbolic
Removed calls to '__const_udelay' (function is undefined)
Removed calls to 'get_random_bytes' (function is undefined)
Removed calls to '__might_fault' (function is undefined)
Removed calls to 'set_disk_ro' (function is undefined)
Removed calls to '__copy_from_user_overflow' (function is undefined)
Defining function fget as symbolic
Defining function revalidate_disk as symbolic
Defining function kobject_uevent as symbolic
Removed calls to 'kobject_init' (function is undefined)
Removed calls to '__list_add_rcu' (function is undefined)
Defining function strreplace as symbolic
Defining function kobject_add as symbolic
Defining function bd_link_disk_holder as symbolic
Defining function blkdev_get_by_dev as symbolic
Defining function __bdevname as symbolic
Defining function _copy_from_user as symbolic
Removed calls to '__copy_to_user_overflow' (function is undefined)
Defining function _copy_to_user as symbolic
Defining function check_disk_change as symbolic
Removed calls to 'blk_cleanup_queue' (function is undefined)
Removed calls to 'del_gendisk' (function is undefined)
Removed calls to 'put_disk' (function is undefined)
Removed calls to 'blk_set_stacking_limits' (function is undefined)
Defining function proc_dointvec as symbolic
Defining function seq_lseek as symbolic
Defining function seq_read as symbolic
Defining function seq_release_private as symbolic
Defining function seq_open as symbolic
Defining function jiffies_to_msecs as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'blk_unregister_region' (function is undefined)
Removed calls to 'unregister_blkdev' (function is undefined)
Removed calls to 'unregister_sysctl_table' (function is undefined)
Removed calls to 'remove_proc_entry' (function is undefined)
Removed calls to 'destroy_workqueue' (function is undefined)
Removed calls to 'blk_register_region' (function is undefined)
Defining function ldv_probe_21 as symbolic
Defining function ldv_probe_51 as symbolic
Removed calls to 'blk_queue_make_request' (function is undefined)
Removed calls to 'blk_queue_flush' (function is undefined)
Removed calls to 'add_disk' (function is undefined)
Defining function blk_alloc_queue as symbolic
Defining function alloc_disk as symbolic
Defining function kobject_init_and_add as symbolic
Defining function __alloc_workqueue_key as symbolic
Defining function register_blkdev as symbolic
Defining function register_reboot_notifier as symbolic
Defining function register_sysctl_table as symbolic
Defining function proc_create_data as symbolic
Defining function unregister_reboot_notifier as symbolic
Defining function queue_delayed_work_on as symbolic
Linked our definitions to these undefined functions:
  memcmp
  strcmp
  strcpy
  strlen
  strncmp
  strncpy
  __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: 1.71754789352
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 954 605 5199 31172
INFO: Starting verification
WARNING: this target does not support the llvm.returnaddress intrinsic.
WARNING: this target does not support the llvm.returnaddress intrinsic.
WARNING: this target does not support the llvm.returnaddress intrinsic.
WARNING: this target does not support the llvm.returnaddress intrinsic.
KLEE: WARNING ONCE: function "md_new_event" has inline asm
KLEE: WARNING ONCE: function "mddev_suspend" has inline asm
KLEE: WARNING ONCE: function "mddev_resume" has inline asm
KLEE: WARNING ONCE: function "md_wakeup_thread" has inline asm
KLEE: WARNING ONCE: function "rcu_read_lock" has inline asm
KLEE: WARNING ONCE: function "rcu_read_unlock" has inline asm
KLEE: WARNING ONCE: function "submit_flushes" has inline asm
KLEE: WARNING ONCE: function "md_end_flush" has inline asm
KLEE: WARNING ONCE: function "rdev_dec_pending" has inline asm
KLEE: WARNING ONCE: function "md_update_sb" has inline asm
KLEE: WARNING ONCE: function "md_error" has inline asm
KLEE: WARNING ONCE: function "bitmap_update_sb" has inline asm
KLEE: WARNING ONCE: function "md_super_write" has inline asm
KLEE: WARNING ONCE: function "super_written" has inline asm
KLEE: WARNING ONCE: function "__kunmap_atomic" has inline asm
KLEE: WARNING ONCE: function "write_page" has inline asm
KLEE: WARNING ONCE: function "rcu_read_unlock___0" has inline asm
KLEE: WARNING ONCE: function "bitmap_file_kick" has inline asm
KLEE: WARNING ONCE: function "md_run" has inline asm
KLEE: WARNING ONCE: function "analyze_sbs" has inline asm
KLEE: WARNING ONCE: function "bitmap_create" has inline asm
KLEE: WARNING ONCE: function "free_buffers" has inline asm
KLEE: WARNING ONCE: function "bitmap_read_sb" has inline asm
KLEE: WARNING ONCE: function "bitmap_resize" has inline asm
KLEE: WARNING ONCE: function "bitmap_get_counter" has inline asm
KLEE: WARNING ONCE: function "bitmap_file_set_bit" has inline asm
KLEE: WARNING ONCE: function "bitmap_unplug" has inline asm
KLEE: WARNING ONCE: function "read_page" has inline asm
KLEE: WARNING ONCE: function "bitmap_print_sb" has inline asm
KLEE: WARNING ONCE: function "end_bitmap_write" has inline asm
KLEE: WARNING ONCE: function "__md_stop_writes" has inline asm
KLEE: WARNING ONCE: function "md_reap_sync_thread" has inline asm
KLEE: WARNING ONCE: function "bitmap_daemon_work" has inline asm
KLEE: WARNING ONCE: function "bitmap_file_clear_bit" has inline asm
KLEE: WARNING ONCE: function "__md_stop" has inline asm
KLEE: WARNING ONCE: function "md_thread" has inline asm
KLEE: WARNING ONCE: function "md_done_sync" has inline asm
KLEE: WARNING ONCE: function "md_write_start" has inline asm
KLEE: WARNING ONCE: function "md_write_end" has inline asm
KLEE: WARNING ONCE: function "md_allow_write" has inline asm
KLEE: WARNING ONCE: function "md_do_sync" has inline asm
KLEE: WARNING ONCE: function "is_mddev_idle" has inline asm
KLEE: WARNING ONCE: function "md_check_recovery" has inline asm
KLEE: WARNING ONCE: function "remove_and_add_spares" has inline asm
KLEE: WARNING ONCE: function "bitmap_write_all" has inline asm
KLEE: WARNING ONCE: function "md_start_sync" has inline asm
KLEE: WARNING ONCE: function "read_seqbegin" has inline asm
KLEE: WARNING ONCE: function "arch_local_irq_restore" has inline asm
KLEE: WARNING ONCE: function "rdev_set_badblocks" has inline asm
KLEE: WARNING ONCE: function "md_reload_sb" has inline asm
KLEE: WARNING ONCE: function "bitmap_startwrite" has inline asm
KLEE: WARNING ONCE: function "bitmap_endwrite" has inline asm
KLEE: WARNING ONCE: function "bitmap_cond_end_sync" has inline asm
KLEE: WARNING ONCE: function "bitmap_load" has inline asm
KLEE: WARNING ONCE: function "bitmap_init_from_disk" has inline asm
KLEE: WARNING ONCE: function "bitmap_copy_from_slot" has inline asm
KLEE: WARNING ONCE: function "super_90_validate" has inline asm
KLEE: WARNING ONCE: function "super_1_validate" has inline asm
KLEE: WARNING ONCE: function "action_store" has inline asm
KLEE: WARNING ONCE: function "md_seq_start" has inline asm
KLEE: WARNING ONCE: function "md_seq_next" has inline asm
KLEE: WARNING ONCE: function "state_store" has inline asm
KLEE: WARNING ONCE: function "add_bound_rdev" has inline asm
KLEE: WARNING ONCE: function "slot_store" has inline asm
KLEE: WARNING ONCE: function "rdev_size_store" has inline asm
KLEE: WARNING ONCE: function "recovery_start_store" has inline asm
KLEE: WARNING ONCE: function "bb_store" has inline asm
KLEE: WARNING ONCE: function "md_notify_reboot" has inline asm
KLEE: WARNING ONCE: function "md_open" has inline asm
KLEE: WARNING ONCE: function "md_release" has inline asm
KLEE: WARNING ONCE: function "md_ioctl" has inline asm
KLEE: WARNING ONCE: function "restart_array" has inline asm
KLEE: WARNING ONCE: function "do_md_stop" has inline asm
KLEE: WARNING ONCE: function "md_set_readonly" has inline asm
KLEE: WARNING ONCE: function "add_new_disk" has inline asm
KLEE: WARNING ONCE: function "mddev_find" has inline asm
KLEE: WARNING ONCE: function "md_attr_show" has inline asm
KLEE: WARNING ONCE: function "md_attr_store" has inline asm
KLEE: WARNING ONCE: function "level_store" has inline asm
KLEE: WARNING ONCE: function "resync_start_store" has inline asm
KLEE: WARNING ONCE: function "array_state_store" has inline asm
KLEE: WARNING ONCE: function "location_store" has inline asm
KLEE: WARNING ONCE: function "main" has inline asm
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_4868d81d-5998-430a-bdf0-109c551b79b9/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-sYoorO/linux-4.2-rc1.tar.xz-32_7a-drivers--md--md-mod.ko-entry_point_true-unreach-call.cil.out.c:21352: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 26186 states (over memory cap)
KLEE: WARNING: killing 49475 states (over memory cap)
KLEE: WARNING: killing 42284 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 46455 states (over memory cap)
KLEE: WARNING: killing 49976 states (over memory cap)
KLEE: WARNING: killing 53517 states (over memory cap)
KLEE: WARNING: killing 55348 states (over memory cap)
KLEE: WARNING: killing 46308 states (over memory cap)
KLEE: WARNING: killing 48708 states (over memory cap)
KLEE: WARNING: killing 51685 states (over memory cap)
KLEE: WARNING: killing 52254 states (over memory cap)
KLEE: WARNING: killing 50229 states (over memory cap)
KLEE: WARNING: killing 49418 states (over memory cap)
KLEE: WARNING: killing 48713 states (over memory cap)
KLEE: WARNING: killing 51931 states (over memory cap)
KLEE: WARNING: killing 47974 states (over memory cap)
KLEE: WARNING: killing 50501 states (over memory cap)
KLEE: WARNING: killing 50750 states (over memory cap)
KLEE: WARNING: killing 50442 states (over memory cap)
KLEE: WARNING: killing 52829 states (over memory cap)
KLEE: WARNING: killing 49510 states (over memory cap)
KLEE: WARNING: killing 48575 states (over memory cap)
KLEE: WARNING: killing 53073 states (over memory cap)
KLEE: WARNING: killing 48193 states (over memory cap)
KLEE: WARNING: killing 51579 states (over memory cap)
KLEE: WARNING: killing 51333 states (over memory cap)
KLEE: WARNING: killing 49082 states (over memory cap)
KLEE: WARNING: killing 50195 states (over memory cap)
KLEE: WARNING: killing 50921 states (over memory cap)
KLEE: WARNING: killing 48775 states (over memory cap)
KLEE: WARNING: killing 51479 states (over memory cap)
KLEE: WARNING: killing 54082 states (over memory cap)
KLEE: WARNING: killing 49140 states (over memory cap)
KLEE: WARNING: killing 48285 states (over memory cap)
KLEE: WARNING: killing 50867 states (over memory cap)
KLEE: WARNING: killing 53319 states (over memory cap)
KLEE: WARNING: killing 47583 states (over memory cap)
KLEE: WARNING: killing 51785 states (over memory cap)
KLEE: WARNING: killing 48918 states (over memory cap)
KLEE: WARNING: killing 50718 states (over memory cap)
KLEE: WARNING: killing 51439 states (over memory cap)
KLEE: WARNING: killing 52229 states (over memory cap)
KLEE: WARNING: killing 49725 states (over memory cap)
KLEE: WARNING: killing 50963 states (over memory cap)
KLEE: WARNING: killing 51165 states (over memory cap)
KLEE: WARNING: killing 50215 states (over memory cap)
KLEE: WARNING: killing 50428 states (over memory cap)
KLEE: WARNING: killing 50944 states (over memory cap)
KLEE: WARNING: killing 51006 states (over memory cap)
KLEE: WARNING: killing 51838 states (over memory cap)
KLEE: WARNING: killing 50284 states (over memory cap)
KLEE: WARNING: killing 49121 states (over memory cap)
KLEE: WARNING: killing 50712 states (over memory cap)
KLEE: WARNING: killing 50211 states (over memory cap)
KLEE: WARNING: killing 51056 states (over memory cap)
KLEE: WARNING: killing 51808 states (over memory cap)
KLEE: WARNING: killing 48491 states (over memory cap)
KLEE: WARNING: killing 50501 states (over memory cap)
KLEE: WARNING: killing 52283 states (over memory cap)
KLEE: WARNING: killing 49004 states (over memory cap)
KLEE: WARNING: killing 21264 states (over memory cap)
KLEE: WARNING: killing 90776 states (over memory cap)
KLEE: WARNING: killing 103450 states (over memory cap)
KLEE: WARNING: killing 84147 states (over memory cap)
KLEE: WARNING: killing 97370 states (over memory cap)
