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-08_1a-drivers--md--md-cluster.ko-entry_point_false-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.: 76 84 504 3274
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 0.233172893524
Removed calls to 'md_wakeup_thread' (function is undefined)
Removed calls to 'complete' (function is undefined)
Defining function printk as symbolic
Removed calls to 'list_del' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Removed calls to 'md_check_recovery' (function is undefined)
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Defining function md_register_thread as symbolic
Defining function snprintf as symbolic
Removed calls to 'wait_for_completion' (function is undefined)
Defining function bitmap_copy_from_slot as symbolic
Removed calls to '__init_waitqueue_head' (function is undefined)
Defining function dlm_lock as symbolic
Defining function strlcpy as symbolic
Removed calls to '__mutex_init' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to 'md_unregister_thread' (function is undefined)
Removed calls to 'md_update_sb' (function is undefined)
Defining function dlm_release_lockspace as symbolic
Defining function dlm_unlock as symbolic
Defining function dlm_new_lockspace as symbolic
Removed calls to 'md_reload_sb' (function is undefined)
Removed calls to 'md_kick_rdev_from_array' (function is undefined)
Defining function md_find_rdev_nr_rcu as symbolic
Defining function kobject_uevent_env as symbolic
Defining function wait_for_completion_timeout as symbolic
Defining function sprintf as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Defining function register_md_cluster_operations as symbolic
Defining function unregister_md_cluster_operations as symbolic
Linked our definitions to these undefined functions:
  strlen
  __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.246370077133
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 121 82 325 2397
INFO: Starting verification
KLEE: WARNING ONCE: function "recover_slot" has inline asm
KLEE: WARNING ONCE: function "recover_bitmaps" has inline asm
KLEE: WARNING ONCE: function "recv_daemon" 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_75d7cda7-179f-456e-b6f0-e3ebd32ba1b5/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-LKQO_Y/linux-4.2-rc1.tar.xz-08_1a-drivers--md--md-cluster.ko-entry_point_false-unreach-call.cil.out.c:4751: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-LKQO_Y/linux-4.2-rc1.tar.xz-08_1a-drivers--md--md-cluster.ko-entry_point_false-unreach-call.cil.out.c:4778: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-LKQO_Y/linux-4.2-rc1.tar.xz-08_1a-drivers--md--md-cluster.ko-entry_point_false-unreach-call.cil.out.c:5385: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-LKQO_Y/linux-4.2-rc1.tar.xz-08_1a-drivers--md--md-cluster.ko-entry_point_false-unreach-call.cil.out.c:4173: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-LKQO_Y/linux-4.2-rc1.tar.xz-08_1a-drivers--md--md-cluster.ko-entry_point_false-unreach-call.cil.out.c:4215: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-LKQO_Y/linux-4.2-rc1.tar.xz-08_1a-drivers--md--md-cluster.ko-entry_point_false-unreach-call.cil.out.c:5421: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-LKQO_Y/linux-4.2-rc1.tar.xz-08_1a-drivers--md--md-cluster.ko-entry_point_false-unreach-call.cil.out.c:5816: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-LKQO_Y/linux-4.2-rc1.tar.xz-08_1a-drivers--md--md-cluster.ko-entry_point_false-unreach-call.cil.out.c:5070: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-LKQO_Y/linux-4.2-rc1.tar.xz-08_1a-drivers--md--md-cluster.ko-entry_point_false-unreach-call.cil.out.c:5434: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-LKQO_Y/linux-4.2-rc1.tar.xz-08_1a-drivers--md--md-cluster.ko-entry_point_false-unreach-call.cil.out.c:5612: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-LKQO_Y/linux-4.2-rc1.tar.xz-08_1a-drivers--md--md-cluster.ko-entry_point_false-unreach-call.cil.out.c:4581: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-LKQO_Y/linux-4.2-rc1.tar.xz-08_1a-drivers--md--md-cluster.ko-entry_point_false-unreach-call.cil.out.c:4258: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-LKQO_Y/linux-4.2-rc1.tar.xz-08_1a-drivers--md--md-cluster.ko-entry_point_false-unreach-call.cil.out.c:4258: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-LKQO_Y/linux-4.2-rc1.tar.xz-08_1a-drivers--md--md-cluster.ko-entry_point_false-unreach-call.cil.out.c:4560: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_75d7cda7-179f-456e-b6f0-e3ebd32ba1b5/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_75d7cda7-179f-456e-b6f0-e3ebd32ba1b5/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_75d7cda7-179f-456e-b6f0-e3ebd32ba1b5/symbiotic/lib/kernel/kfree.c:5: free of alloca
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-LKQO_Y/linux-4.2-rc1.tar.xz-08_1a-drivers--md--md-cluster.ko-entry_point_false-unreach-call.cil.out.c:4563: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_75d7cda7-179f-456e-b6f0-e3ebd32ba1b5/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_75d7cda7-179f-456e-b6f0-e3ebd32ba1b5/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_75d7cda7-179f-456e-b6f0-e3ebd32ba1b5/symbiotic/lib/kernel/kfree.c:5: free of alloca
KLEE: NOTE: now ignoring this error at this location
