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--dm-raid.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.: 164 141 1512 8323
Removed infinite loop in read_disk_sb
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.348974943161
Removed calls to 'mddev_init' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to 'md_error' (function is undefined)
Removed calls to 'dm_put_device' (function is undefined)
Removed calls to 'put_page' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to 'mddev_unlock' (function is undefined)
Removed calls to 'md_stop' (function is undefined)
Removed calls to 'dm_table_add_target_callbacks' (function is undefined)
Removed calls to 'mddev_suspend' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to 'md_stop_writes' (function is undefined)
Removed calls to 'mddev_resume' (function is undefined)
Removed calls to 'md_reap_sync_thread' (function is undefined)
Removed calls to 'md_wakeup_thread' (function is undefined)
Removed calls to 'blk_limits_io_min' (function is undefined)
Removed calls to 'blk_limits_io_opt' (function is undefined)
Defining function strcasecmp as symbolic
Defining function printk as symbolic
Defining function scnprintf as symbolic
Defining function bitmap_load as symbolic
Defining function sync_page_io as symbolic
Removed calls to 'md_rdev_clear' (function is undefined)
Removed calls to 'dm_table_event' (function is undefined)
Defining function md_run as symbolic
Defining function mddev_congested as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Defining function dm_table_get_mode as symbolic
Defining function dm_get_device as symbolic
Defining function alloc_pages_current as symbolic
Defining function raid5_set_cache_size as symbolic
Defining function dm_set_target_max_io_len as symbolic
Defining function md_rdev_init as symbolic
Defining function kstrtoull as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'dm_unregister_target' (function is undefined)
Defining function ldv_preresume_2 as symbolic
Defining function dm_register_target as symbolic
Defining function queue_work_on as symbolic
Defining function queue_delayed_work_on as symbolic
Removed calls to 'flush_workqueue' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function mutex_trylock as symbolic
Defining function mutex_lock_interruptible as symbolic
Linked our definitions to these undefined functions:
  strcmp
  __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.402709960938
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 213 129 974 4940
INFO: Starting verification
KLEE: WARNING ONCE: function "raid_ctr" has inline asm
KLEE: WARNING ONCE: function "raid_resume" has inline asm
KLEE: WARNING ONCE: function "raid_status" has inline asm
KLEE: WARNING ONCE: function "raid_message" has inline asm
KLEE: WARNING ONCE: function "super_validate" 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_bfbb2cd4-9d28-4f13-a8e7-a172ec1e0564/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-S1mF7m/linux-4.2-rc1.tar.xz-32_7a-drivers--md--dm-raid.ko-entry_point_false-unreach-call.cil.out.c:6919: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-S1mF7m/linux-4.2-rc1.tar.xz-32_7a-drivers--md--dm-raid.ko-entry_point_false-unreach-call.cil.out.c:7072: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-S1mF7m/linux-4.2-rc1.tar.xz-32_7a-drivers--md--dm-raid.ko-entry_point_false-unreach-call.cil.out.c:6375: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-S1mF7m/linux-4.2-rc1.tar.xz-32_7a-drivers--md--dm-raid.ko-entry_point_false-unreach-call.cil.out.c:6902: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 14764 states (over memory cap)
KLEE: WARNING: killing 12389 states (over memory cap)
KLEE: WARNING: killing 12442 states (over memory cap)
KLEE: WARNING: killing 12206 states (over memory cap)
KLEE: WARNING: killing 11871 states (over memory cap)
KLEE: WARNING: killing 12591 states (over memory cap)
KLEE: WARNING: killing 11988 states (over memory cap)
KLEE: WARNING: killing 12234 states (over memory cap)
KLEE: WARNING: killing 12284 states (over memory cap)
KLEE: WARNING: killing 12243 states (over memory cap)
KLEE: WARNING: killing 12965 states (over memory cap)
KLEE: WARNING: killing 13303 states (over memory cap)
KLEE: WARNING: killing 13082 states (over memory cap)
KLEE: WARNING: killing 12675 states (over memory cap)
KLEE: WARNING: killing 12833 states (over memory cap)
KLEE: WARNING: killing 12897 states (over memory cap)
KLEE: WARNING: killing 12312 states (over memory cap)
KLEE: WARNING: killing 12376 states (over memory cap)
KLEE: WARNING: killing 12248 states (over memory cap)
KLEE: WARNING: killing 12768 states (over memory cap)
KLEE: WARNING: killing 12556 states (over memory cap)
KLEE: WARNING: killing 12338 states (over memory cap)
KLEE: WARNING: killing 12584 states (over memory cap)
KLEE: WARNING: killing 13094 states (over memory cap)
KLEE: WARNING: killing 12614 states (over memory cap)
KLEE: WARNING: killing 13036 states (over memory cap)
KLEE: WARNING: killing 12371 states (over memory cap)
KLEE: WARNING: killing 12517 states (over memory cap)
KLEE: WARNING: killing 12759 states (over memory cap)
KLEE: WARNING: killing 13091 states (over memory cap)
KLEE: WARNING: killing 12789 states (over memory cap)
KLEE: WARNING: killing 12857 states (over memory cap)
KLEE: WARNING: killing 12650 states (over memory cap)
KLEE: WARNING: killing 12703 states (over memory cap)
KLEE: WARNING: killing 13215 states (over memory cap)
KLEE: WARNING: killing 12829 states (over memory cap)
KLEE: WARNING: killing 12542 states (over memory cap)
KLEE: WARNING: killing 13216 states (over memory cap)
KLEE: WARNING: killing 12659 states (over memory cap)
KLEE: WARNING: killing 12895 states (over memory cap)
KLEE: WARNING: killing 12075 states (over memory cap)
KLEE: WARNING: killing 12216 states (over memory cap)
KLEE: WARNING: killing 12102 states (over memory cap)
KLEE: WARNING: killing 12251 states (over memory cap)
KLEE: WARNING: killing 12131 states (over memory cap)
KLEE: WARNING: killing 12973 states (over memory cap)
KLEE: WARNING: killing 12866 states (over memory cap)
KLEE: WARNING: killing 12934 states (over memory cap)
KLEE: WARNING: killing 12642 states (over memory cap)
KLEE: WARNING: killing 12185 states (over memory cap)
KLEE: WARNING: killing 12417 states (over memory cap)
KLEE: WARNING: killing 13081 states (over memory cap)
KLEE: WARNING: killing 12711 states (over memory cap)
KLEE: WARNING: killing 12689 states (over memory cap)
KLEE: WARNING: killing 12147 states (over memory cap)
KLEE: WARNING: killing 12634 states (over memory cap)
KLEE: WARNING: killing 12781 states (over memory cap)
KLEE: WARNING: killing 12247 states (over memory cap)
KLEE: WARNING: killing 12647 states (over memory cap)
KLEE: WARNING: killing 12543 states (over memory cap)
KLEE: WARNING: killing 12515 states (over memory cap)
KLEE: WARNING: killing 12824 states (over memory cap)
KLEE: WARNING: killing 13059 states (over memory cap)
KLEE: WARNING: killing 12784 states (over memory cap)
KLEE: WARNING: killing 12427 states (over memory cap)
KLEE: WARNING: killing 12566 states (over memory cap)
KLEE: WARNING: killing 12712 states (over memory cap)
KLEE: WARNING: killing 12769 states (over memory cap)
KLEE: WARNING: killing 12579 states (over memory cap)
KLEE: WARNING: killing 12558 states (over memory cap)
KLEE: WARNING: killing 12783 states (over memory cap)
KLEE: WARNING: killing 12679 states (over memory cap)
KLEE: WARNING: killing 12577 states (over memory cap)
KLEE: WARNING: killing 12636 states (over memory cap)
KLEE: WARNING: killing 12611 states (over memory cap)
KLEE: WARNING: killing 12595 states (over memory cap)
KLEE: WARNING: killing 12482 states (over memory cap)
KLEE: WARNING: killing 12290 states (over memory cap)
KLEE: WARNING: killing 11942 states (over memory cap)
KLEE: WARNING: killing 12405 states (over memory cap)
KLEE: WARNING: killing 13034 states (over memory cap)
KLEE: WARNING: killing 12608 states (over memory cap)
KLEE: WARNING: killing 12581 states (over memory cap)
KLEE: WARNING: killing 12561 states (over memory cap)
KLEE: WARNING: killing 12699 states (over memory cap)
KLEE: WARNING: killing 12922 states (over memory cap)
KLEE: WARNING: killing 13309 states (over memory cap)
KLEE: WARNING: killing 12891 states (over memory cap)
KLEE: WARNING: killing 12789 states (over memory cap)
KLEE: WARNING: killing 12196 states (over memory cap)
KLEE: WARNING: killing 12497 states (over memory cap)
KLEE: WARNING: killing 12796 states (over memory cap)
KLEE: WARNING: killing 12372 states (over memory cap)
KLEE: WARNING: killing 12273 states (over memory cap)
KLEE: WARNING: killing 12652 states (over memory cap)
KLEE: WARNING: killing 12788 states (over memory cap)
KLEE: WARNING: killing 12608 states (over memory cap)
KLEE: WARNING: killing 12744 states (over memory cap)
KLEE: WARNING: killing 12725 states (over memory cap)
KLEE: WARNING: killing 12546 states (over memory cap)
KLEE: WARNING: killing 12523 states (over memory cap)
KLEE: WARNING: killing 12814 states (over memory cap)
KLEE: WARNING: killing 12552 states (over memory cap)
KLEE: WARNING: killing 12924 states (over memory cap)
KLEE: WARNING: killing 12278 states (over memory cap)
KLEE: WARNING: killing 12416 states (over memory cap)
KLEE: WARNING: killing 12322 states (over memory cap)
KLEE: WARNING: killing 12613 states (over memory cap)
KLEE: WARNING: killing 12441 states (over memory cap)
KLEE: WARNING: killing 12412 states (over memory cap)
KLEE: WARNING: killing 12313 states (over memory cap)
KLEE: WARNING: killing 11982 states (over memory cap)
KLEE: WARNING: killing 12271 states (over memory cap)
KLEE: WARNING: killing 12482 states (over memory cap)
KLEE: WARNING: killing 12924 states (over memory cap)
KLEE: WARNING: killing 12288 states (over memory cap)
KLEE: WARNING: killing 12737 states (over memory cap)
KLEE: WARNING: killing 12794 states (over memory cap)
KLEE: WARNING: killing 12552 states (over memory cap)
KLEE: WARNING: killing 12455 states (over memory cap)
KLEE: WARNING: killing 12281 states (over memory cap)
KLEE: WARNING: killing 12568 states (over memory cap)
