bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-challenges/linux-3.8-rc1-32_7a-drivers--md--md-mod.ko-ldv_main0_sequence_infinite_withcheck_stateful_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.: 461 492 6397 39857
Removed infinite loop in write_page
Removed infinite loop in sync_super
Removed infinite loop in md_open
Removed infinite loop in md_release
Removed infinite loop in md_ioctl
Removed infinite loop in bitmap_create
Removed infinite loop in free_buffers
Removed infinite loop in get_page
Removed infinite loop in bitmap_new_disk_sb
Removed infinite loop in mddev_suspend
Removed infinite loop in md_write_start
INFO: Compilation, preparation and instrumentation time: 1.24618601799
Removed calls to 'submit_bio' (function is undefined)
Removed calls to 'prepare_to_wait' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Defining function autoremove_wake_function as symbolic
Defining function bio_add_page as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Removed calls to 'bio_put' (function is undefined)
Defining function printk as symbolic
Removed calls to 'sysfs_notify_dirent' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function queue_work_on as symbolic
Defining function bdevname as symbolic
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to 'bioset_free' (function is undefined)
Defining function _atomic_dec_and_lock as symbolic
Removed calls to 'sysfs_remove_group' (function is undefined)
Removed calls to 'kobject_del' (function is undefined)
Removed calls to 'kobject_put' (function is undefined)
Defining function bio_alloc_bioset as symbolic
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'wait_for_completion' (function is undefined)
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Removed calls to 'complete' (function is undefined)
Defining function alloc_pages_current as symbolic
Removed calls to 'sysfs_notify' (function is undefined)
Defining function get_seconds as symbolic
Removed calls to 'lock_acquire' (function is undefined)
Removed calls to 'lockdep_rcu_suspicious' (function is undefined)
Defining function submit_bh as symbolic
Defining function d_path as symbolic
Defining function debug_lockdep_rcu_enabled as symbolic
Removed calls to 'lock_release' (function is undefined)
Defining function rcu_is_cpu_idle as symbolic
Defining function rcu_lockdep_current_cpu_online as symbolic
Defining function lock_is_held as symbolic
Defining function kthread_stop as symbolic
Defining function sprintf as symbolic
Defining function simple_strtoul as symbolic
Defining function kstrtoll as symbolic
Defining function kstrtoull as symbolic
Defining function simple_strtoull as symbolic
Defining function skip_spaces as symbolic
Removed calls to 'flush_workqueue' (function is undefined)
Removed calls to 'might_fault' (function is undefined)
Removed calls to 'get_random_bytes' (function is undefined)
Removed calls to 'set_disk_ro' (function is undefined)
Removed calls to 'fput' (function is undefined)
Defining function capable as symbolic
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Removed calls to 'blk_integrity_unregister' (function is undefined)
Removed calls to 'sysfs_put' (function is undefined)
Defining function fget as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'free_buffer_head' (function is undefined)
Removed calls to 'put_page' (function is undefined)
Defining function invalidate_mapping_pages as symbolic
Defining function alloc_page_buffers as symbolic
Defining function bmap as symbolic
Defining function __get_page_tail as symbolic
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Defining function sysfs_get_dirent as symbolic
Defining function vfs_fsync as symbolic
Removed calls to 'invalidate_bdev' (function is undefined)
Removed calls to 'module_put' (function is undefined)
Defining function revalidate_disk as symbolic
Defining function kobject_uevent as symbolic
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
Defining function sysfs_create_group as symbolic
Defining function sysfs_create_link as symbolic
Removed calls to 'bd_unlink_disk_holder' (function is undefined)
Removed calls to 'sysfs_remove_link' (function is undefined)
Removed calls to 'synchronize_sched' (function is undefined)
Removed calls to 'blkdev_put' (function is undefined)
Defining function kobject_get as symbolic
Removed calls to 'kobject_init' (function is undefined)
Removed calls to '__list_add_rcu' (function is undefined)
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 del_timer_sync as symbolic
Defining function _copy_to_user as symbolic
Defining function _copy_from_user as symbolic
Defining function mutex_lock_interruptible as symbolic
Removed calls to '__list_add' (function is undefined)
Defining function check_disk_change as symbolic
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'init_timer_key' (function is undefined)
Removed calls to 'del_gendisk' (function is undefined)
Removed calls to 'put_disk' (function is undefined)
Removed calls to 'blk_cleanup_queue' (function is undefined)
Defining function sscanf as symbolic
Defining function snprintf as symbolic
Removed calls to '__const_udelay' (function is undefined)
Defining function mutex_trylock as symbolic
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 seq_printf as symbolic
Defining function seq_path as symbolic
Defining function jiffies_to_msecs as symbolic
Defining function bio_clone_bioset as symbolic
Removed calls to 'bio_advance' (function is undefined)
Removed calls to 'bio_endio' (function is undefined)
Defining function blk_integrity_compare as symbolic
Defining function blk_integrity_register as symbolic
Defining function bioset_integrity_create as symbolic
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 allow_signal as symbolic
Defining function kthread_should_stop as symbolic
Defining function schedule_timeout as symbolic
Defining function mod_timer as symbolic
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 _cond_resched as symbolic
Defining function find_next_bit as symbolic
Defining function msecs_to_jiffies as symbolic
Removed calls to 'ldv_handler_precall' (function is undefined)
Removed calls to 'unregister_blkdev' (function is undefined)
Removed calls to 'destroy_workqueue' (function is undefined)
Removed calls to 'blk_register_region' (function is undefined)
Removed calls to 'ldv_check_return_value' (function is undefined)
Removed calls to 'blk_unregister_region' (function is undefined)
Removed calls to 'unregister_sysctl_table' (function is undefined)
Removed calls to 'remove_proc_entry' (function is undefined)
Defining function unregister_reboot_notifier as symbolic
Defining function __alloc_workqueue_key as symbolic
Defining function register_blkdev as symbolic
Removed calls to 'blk_queue_make_request' (function is undefined)
Removed calls to 'blk_set_stacking_limits' (function is undefined)
Removed calls to 'blk_queue_flush' (function is undefined)
Removed calls to 'add_disk' (function is undefined)
Defining function register_reboot_notifier as symbolic
Defining function register_sysctl_table as symbolic
Defining function proc_create_data as symbolic
Defining function blk_alloc_queue as symbolic
Defining function alloc_disk as symbolic
Defining function kobject_init_and_add as symbolic
Linked our definitions to these undefined functions:
  memcmp
  strchr
  strcmp
  strcpy
  strncmp
  strncpy
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 1.27586317062
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 642 409 4017 24559
INFO: Starting verification
KLEE: WARNING ONCE: function "super_90_validate" has inline asm
KLEE: WARNING ONCE: function "super_1_validate" has inline asm
KLEE: WARNING ONCE: function "super_1_sync" has inline asm
KLEE: WARNING ONCE: function "md_super_write" has inline asm
KLEE: WARNING ONCE: function "md_super_wait" has inline asm
KLEE: WARNING ONCE: function "super_written" has inline asm
KLEE: WARNING ONCE: function "md_error" has inline asm
KLEE: WARNING ONCE: function "md_print_devices" has inline asm
KLEE: WARNING ONCE: function "md_wakeup_thread" has inline asm
KLEE: WARNING ONCE: function "bitmap_print_sb" has inline asm
KLEE: WARNING ONCE: function "action_store" has inline asm
KLEE: WARNING ONCE: function "md_reap_sync_thread" has inline asm
KLEE: WARNING ONCE: function "md_update_sb" has inline asm
KLEE: WARNING ONCE: function "bitmap_update_sb" has inline asm
KLEE: WARNING ONCE: function "write_page" has inline asm
KLEE: WARNING ONCE: function "rdev_dec_pending" 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 "bitmap_unplug" has inline asm
KLEE: WARNING ONCE: function "bitmap_file_set_bit" 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 "rcu_read_lock" has inline asm
KLEE: WARNING ONCE: function "rcu_read_unlock" has inline asm
KLEE: WARNING ONCE: function "bitmap_create" has inline asm
KLEE: WARNING ONCE: function "bitmap_load" has inline asm
KLEE: WARNING ONCE: function "md_allow_write" 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 "remove_and_add_spares" has inline asm
KLEE: WARNING ONCE: function "add_new_disk" has inline asm
KLEE: WARNING ONCE: function "md_run" has inline asm
KLEE: WARNING ONCE: function "__md_stop_writes" has inline asm
KLEE: WARNING ONCE: function "bitmap_daemon_work" has inline asm
KLEE: WARNING ONCE: function "__md_stop" has inline asm
KLEE: WARNING ONCE: function "bitmap_free" has inline asm
KLEE: WARNING ONCE: function "free_buffers" has inline asm
KLEE: WARNING ONCE: function "read_page" has inline asm
KLEE: WARNING ONCE: function "end_bitmap_write" has inline asm
KLEE: WARNING ONCE: function "bitmap_resize" 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 "mddev_suspend" has inline asm
KLEE: WARNING ONCE: function "mddev_resume" has inline asm
KLEE: WARNING ONCE: function "resync_start_store" has inline asm
KLEE: WARNING ONCE: function "state_store" 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 "badblocks_show" has inline asm
KLEE: WARNING ONCE: function "array_state_store" has inline asm
KLEE: WARNING ONCE: function "md_notify_reboot" 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 "location_store" has inline asm
KLEE: WARNING ONCE: function "md_new_event" has inline asm
KLEE: WARNING ONCE: function "md_trim_bio" has inline asm
KLEE: WARNING ONCE: function "md_flush_request" 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 "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_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 "bitmap_write_all" has inline asm
KLEE: WARNING ONCE: function "md_wait_for_blocked_rdev" has inline asm
KLEE: WARNING ONCE: function "md_is_badblock" has inline asm
KLEE: WARNING ONCE: function "rdev_set_badblocks" has inline asm
KLEE: WARNING ONCE: function "main" 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: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_05b7bc10-3771-45a0-950d-9bbf8a69ce19/symbiotic/lib/kernel/kfree.c:5: memory error: invalid pointer: free
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_05b7bc10-3771-45a0-950d-9bbf8a69ce19/symbiotic/lib/kernel/kfree.c:5: free of global
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_05b7bc10-3771-45a0-950d-9bbf8a69ce19/symbiotic/lib/kernel/kfree.c:5: free of alloca
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: flushing 9592 bytes on read, may be slow and/or crash: MO103[9592] allocated at global:
KLEE: ERROR: /tmp/symbiotic-mZU9ZD/linux-3.8-rc1-32_7a-drivers--md--md-mod.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:14713: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mZU9ZD/linux-3.8-rc1-32_7a-drivers--md--md-mod.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:14270: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mZU9ZD/linux-3.8-rc1-32_7a-drivers--md--md-mod.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:9872: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mZU9ZD/linux-3.8-rc1-32_7a-drivers--md--md-mod.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:4134: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mZU9ZD/linux-3.8-rc1-32_7a-drivers--md--md-mod.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:14714: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mZU9ZD/linux-3.8-rc1-32_7a-drivers--md--md-mod.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:14714: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mZU9ZD/linux-3.8-rc1-32_7a-drivers--md--md-mod.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:15170: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mZU9ZD/linux-3.8-rc1-32_7a-drivers--md--md-mod.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:9873: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mZU9ZD/linux-3.8-rc1-32_7a-drivers--md--md-mod.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:12507: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mZU9ZD/linux-3.8-rc1-32_7a-drivers--md--md-mod.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:15225: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mZU9ZD/linux-3.8-rc1-32_7a-drivers--md--md-mod.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:9828: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mZU9ZD/linux-3.8-rc1-32_7a-drivers--md--md-mod.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:15458: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mZU9ZD/linux-3.8-rc1-32_7a-drivers--md--md-mod.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:12191: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mZU9ZD/linux-3.8-rc1-32_7a-drivers--md--md-mod.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:9829: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mZU9ZD/linux-3.8-rc1-32_7a-drivers--md--md-mod.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:12237: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mZU9ZD/linux-3.8-rc1-32_7a-drivers--md--md-mod.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:12290: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mZU9ZD/linux-3.8-rc1-32_7a-drivers--md--md-mod.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:14639: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mZU9ZD/linux-3.8-rc1-32_7a-drivers--md--md-mod.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:15459: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mZU9ZD/linux-3.8-rc1-32_7a-drivers--md--md-mod.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:12295: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mZU9ZD/linux-3.8-rc1-32_7a-drivers--md--md-mod.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:14270: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mZU9ZD/linux-3.8-rc1-32_7a-drivers--md--md-mod.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:3992: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mZU9ZD/linux-3.8-rc1-32_7a-drivers--md--md-mod.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:14271: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mZU9ZD/linux-3.8-rc1-32_7a-drivers--md--md-mod.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:14271: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mZU9ZD/linux-3.8-rc1-32_7a-drivers--md--md-mod.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:14272: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mZU9ZD/linux-3.8-rc1-32_7a-drivers--md--md-mod.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:12498: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
