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--vfio--vfio.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.: 74 138 927 6268
Removed infinite loop in vfio_iommu_group_notifier
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 0.296662092209
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'device_destroy' (function is undefined)
Removed calls to 'idr_remove' (function is undefined)
Removed calls to 'iommu_group_put' (function is undefined)
Defining function iommu_group_unregister_notifier as symbolic
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Defining function iommu_group_get as symbolic
Defining function iommu_group_id as symbolic
Defining function iommu_group_register_notifier as symbolic
Defining function device_create as symbolic
Defining function idr_alloc as symbolic
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to 'dev_warn' (function is undefined)
Defining function prepare_to_wait_event as symbolic
Defining function schedule_timeout as symbolic
Defining function iommu_group_for_each_dev as symbolic
Removed calls to 'down_write' (function is undefined)
Removed calls to 'up_write' (function is undefined)
Removed calls to 'down_read' (function is undefined)
Removed calls to 'up_read' (function is undefined)
Removed calls to '__might_fault' (function is undefined)
Removed calls to 'fput' (function is undefined)
Removed calls to 'put_unused_fd' (function is undefined)
Removed calls to 'fd_install' (function is undefined)
Defining function debug_lockdep_rcu_enabled as symbolic
Defining function idr_find_slowpath as symbolic
Defining function strndup_user as symbolic
Defining function get_unused_fd_flags as symbolic
Defining function anon_inode_getfile as symbolic
Defining function __fdget as symbolic
Defining function _copy_to_user as symbolic
Defining function _copy_from_user as symbolic
Removed calls to '__init_rwsem' (function is undefined)
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'idr_destroy' (function is undefined)
Removed calls to 'cdev_del' (function is undefined)
Removed calls to 'unregister_chrdev_region' (function is undefined)
Removed calls to 'class_destroy' (function is undefined)
Removed calls to 'idr_init' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'cdev_init' (function is undefined)
Defining function ldv_open_1 as symbolic
Defining function printk as symbolic
Defining function __class_create as symbolic
Defining function alloc_chrdev_region as symbolic
Defining function cdev_add as symbolic
Defining function __request_module as symbolic
Defining function misc_deregister as symbolic
Defining function kasprintf as symbolic
Defining function misc_register 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.313179016113
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 144 115 565 3563
INFO: Starting verification
KLEE: WARNING ONCE: function "kref_put_mutex" has inline asm
KLEE: WARNING ONCE: function "vfio_iommu_group_notifier" has inline asm
KLEE: WARNING ONCE: function "kref_get" has inline asm
KLEE: WARNING ONCE: function "vfio_del_group_dev" has inline asm
KLEE: WARNING ONCE: function "vfio_group_get_external_user" has inline asm
KLEE: WARNING ONCE: function "vfio_group_try_dissolve_container" has inline asm
KLEE: WARNING ONCE: function "vfio_container_put" has inline asm
KLEE: WARNING ONCE: function "vfio_group_fops_unl_ioctl" has inline asm
KLEE: WARNING ONCE: function "vfio_group_fops_open" has inline asm
KLEE: WARNING ONCE: function "vfio_group_fops_release" 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_08cc02e9-735c-4a04-951e-9f338ab93299/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-rLOJPs/linux-4.2-rc1.tar.xz-08_1a-drivers--vfio--vfio.ko-entry_point_false-unreach-call.cil.out.c:6460: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 13394 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 12105 states (over memory cap)
KLEE: WARNING: killing 12367 states (over memory cap)
KLEE: WARNING: killing 12321 states (over memory cap)
KLEE: WARNING: killing 12740 states (over memory cap)
KLEE: WARNING: killing 12701 states (over memory cap)
KLEE: WARNING: killing 12361 states (over memory cap)
KLEE: WARNING: killing 12777 states (over memory cap)
KLEE: WARNING: killing 13424 states (over memory cap)
KLEE: WARNING: killing 13237 states (over memory cap)
KLEE: WARNING: killing 13580 states (over memory cap)
KLEE: WARNING: killing 13162 states (over memory cap)
KLEE: WARNING: killing 13129 states (over memory cap)
KLEE: WARNING: killing 13621 states (over memory cap)
KLEE: WARNING: killing 13442 states (over memory cap)
KLEE: WARNING: killing 13486 states (over memory cap)
KLEE: WARNING: killing 12849 states (over memory cap)
KLEE: WARNING: killing 13335 states (over memory cap)
KLEE: WARNING: killing 13304 states (over memory cap)
KLEE: WARNING: killing 13421 states (over memory cap)
KLEE: WARNING: killing 13540 states (over memory cap)
KLEE: WARNING: killing 13135 states (over memory cap)
KLEE: WARNING: killing 13316 states (over memory cap)
KLEE: WARNING: killing 13290 states (over memory cap)
KLEE: WARNING: killing 13628 states (over memory cap)
KLEE: WARNING: killing 13814 states (over memory cap)
KLEE: WARNING: killing 13413 states (over memory cap)
KLEE: WARNING: killing 13247 states (over memory cap)
KLEE: WARNING: killing 13496 states (over memory cap)
KLEE: WARNING: killing 13685 states (over memory cap)
KLEE: WARNING: killing 7281 states (over memory cap)
KLEE: WARNING: killing 13140 states (over memory cap)
KLEE: WARNING: killing 7184 states (over memory cap)
KLEE: WARNING: killing 13678 states (over memory cap)
KLEE: WARNING: killing 13639 states (over memory cap)
KLEE: WARNING: killing 13400 states (over memory cap)
KLEE: WARNING: killing 13371 states (over memory cap)
KLEE: WARNING: killing 7184 states (over memory cap)
KLEE: WARNING: killing 13112 states (over memory cap)
KLEE: WARNING: killing 7230 states (over memory cap)
KLEE: WARNING: killing 13218 states (over memory cap)
KLEE: WARNING: killing 7211 states (over memory cap)
KLEE: WARNING: killing 13330 states (over memory cap)
KLEE: WARNING: killing 7264 states (over memory cap)
KLEE: WARNING: killing 13215 states (over memory cap)
KLEE: WARNING: killing 7030 states (over memory cap)
KLEE: WARNING: killing 13099 states (over memory cap)
KLEE: WARNING: killing 7076 states (over memory cap)
KLEE: WARNING: killing 12991 states (over memory cap)
KLEE: WARNING: killing 7405 states (over memory cap)
KLEE: WARNING: killing 13095 states (over memory cap)
KLEE: WARNING: killing 6967 states (over memory cap)
KLEE: WARNING: killing 13195 states (over memory cap)
KLEE: WARNING: killing 7362 states (over memory cap)
KLEE: WARNING: killing 12876 states (over memory cap)
KLEE: WARNING: killing 7132 states (over memory cap)
KLEE: WARNING: killing 12560 states (over memory cap)
KLEE: WARNING: killing 7314 states (over memory cap)
KLEE: WARNING: killing 13146 states (over memory cap)
KLEE: WARNING: killing 6951 states (over memory cap)
KLEE: WARNING: killing 13041 states (over memory cap)
KLEE: WARNING: killing 7613 states (over memory cap)
KLEE: WARNING: killing 6925 states (over memory cap)
KLEE: WARNING: killing 13138 states (over memory cap)
KLEE: WARNING: killing 7176 states (over memory cap)
KLEE: WARNING: killing 6831 states (over memory cap)
KLEE: WARNING: killing 12949 states (over memory cap)
KLEE: WARNING: killing 7353 states (over memory cap)
KLEE: WARNING: killing 7077 states (over memory cap)
KLEE: WARNING: killing 12974 states (over memory cap)
KLEE: WARNING: killing 7329 states (over memory cap)
KLEE: WARNING: killing 6982 states (over memory cap)
KLEE: WARNING: killing 12575 states (over memory cap)
KLEE: WARNING: killing 7231 states (over memory cap)
KLEE: WARNING: killing 12879 states (over memory cap)
KLEE: WARNING: killing 7345 states (over memory cap)
KLEE: WARNING: killing 6806 states (over memory cap)
KLEE: WARNING: killing 6799 states (over memory cap)
KLEE: WARNING: killing 6926 states (over memory cap)
KLEE: WARNING: killing 6855 states (over memory cap)
KLEE: WARNING: killing 6781 states (over memory cap)
KLEE: WARNING: killing 12796 states (over memory cap)
KLEE: WARNING: killing 7562 states (over memory cap)
KLEE: WARNING: killing 6755 states (over memory cap)
KLEE: WARNING: killing 12752 states (over memory cap)
KLEE: WARNING: killing 7335 states (over memory cap)
KLEE: WARNING: killing 6666 states (over memory cap)
KLEE: WARNING: killing 6723 states (over memory cap)
KLEE: WARNING: killing 6853 states (over memory cap)
KLEE: WARNING: killing 6780 states (over memory cap)
KLEE: WARNING: killing 6642 states (over memory cap)
KLEE: WARNING: killing 6833 states (over memory cap)
KLEE: WARNING: killing 6894 states (over memory cap)
KLEE: WARNING: killing 12771 states (over memory cap)
KLEE: WARNING: killing 7271 states (over memory cap)
KLEE: WARNING: killing 6871 states (over memory cap)
KLEE: WARNING: killing 6861 states (over memory cap)
KLEE: WARNING: killing 6856 states (over memory cap)
KLEE: WARNING: killing 6720 states (over memory cap)
KLEE: WARNING: killing 6782 states (over memory cap)
KLEE: WARNING: killing 6973 states (over memory cap)
KLEE: WARNING: killing 6705 states (over memory cap)
KLEE: WARNING: killing 6569 states (over memory cap)
KLEE: WARNING: killing 6561 states (over memory cap)
KLEE: WARNING: killing 6686 states (over memory cap)
KLEE: WARNING: killing 6942 states (over memory cap)
KLEE: WARNING: killing 6873 states (over memory cap)
KLEE: WARNING: killing 6671 states (over memory cap)
KLEE: WARNING: killing 6796 states (over memory cap)
KLEE: WARNING: killing 6725 states (over memory cap)
KLEE: WARNING: killing 6849 states (over memory cap)
KLEE: WARNING: killing 6648 states (over memory cap)
KLEE: WARNING: killing 6638 states (over memory cap)
KLEE: WARNING: killing 6569 states (over memory cap)
KLEE: WARNING: killing 6821 states (over memory cap)
KLEE: WARNING: killing 6687 states (over memory cap)
KLEE: WARNING: killing 7135 states (over memory cap)
KLEE: WARNING: killing 6807 states (over memory cap)
KLEE: WARNING: killing 6927 states (over memory cap)
KLEE: WARNING: killing 6860 states (over memory cap)
KLEE: WARNING: killing 6920 states (over memory cap)
KLEE: WARNING: killing 6720 states (over memory cap)
KLEE: WARNING: killing 6523 states (over memory cap)
KLEE: WARNING: killing 6966 states (over memory cap)
KLEE: WARNING: killing 6896 states (over memory cap)
KLEE: WARNING: killing 6508 states (over memory cap)
KLEE: WARNING: killing 6953 states (over memory cap)
KLEE: WARNING: killing 6755 states (over memory cap)
KLEE: WARNING: killing 6557 states (over memory cap)
KLEE: WARNING: killing 6422 states (over memory cap)
KLEE: WARNING: killing 6673 states (over memory cap)
KLEE: WARNING: killing 6476 states (over memory cap)
KLEE: WARNING: killing 6787 states (over memory cap)
KLEE: WARNING: killing 6911 states (over memory cap)
KLEE: WARNING: killing 6775 states (over memory cap)
KLEE: WARNING: killing 6833 states (over memory cap)
KLEE: WARNING: killing 6828 states (over memory cap)
KLEE: WARNING: killing 6949 states (over memory cap)
KLEE: WARNING: killing 6881 states (over memory cap)
KLEE: WARNING: killing 6368 states (over memory cap)
KLEE: WARNING: killing 6869 states (over memory cap)
KLEE: WARNING: killing 7119 states (over memory cap)
KLEE: WARNING: killing 6608 states (over memory cap)
KLEE: WARNING: killing 6728 states (over memory cap)
KLEE: WARNING: killing 6787 states (over memory cap)
KLEE: WARNING: killing 6591 states (over memory cap)
KLEE: WARNING: killing 6714 states (over memory cap)
KLEE: WARNING: killing 6705 states (over memory cap)
KLEE: WARNING: killing 6510 states (over memory cap)
KLEE: WARNING: killing 6756 states (over memory cap)
KLEE: WARNING: killing 6688 states (over memory cap)
KLEE: WARNING: killing 6873 states (over memory cap)
KLEE: WARNING: killing 6617 states (over memory cap)
KLEE: WARNING: killing 6863 states (over memory cap)
KLEE: WARNING: killing 6733 states (over memory cap)
KLEE: WARNING: killing 6853 states (over memory cap)
KLEE: WARNING: killing 6784 states (over memory cap)
KLEE: WARNING: killing 6904 states (over memory cap)
