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--staging--comedi--comedi.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.: 260 246 2744 18055
Removed infinite loop in comedi_dev_get_from_board_minor
Removed infinite loop in comedi_dev_get_from_subdevice_minor
Removed infinite loop in comedi_free_subdevice_minor
Removed infinite loop in comedi_subdevice_from_minor
Removed infinite loop in ldv_stop
Removed infinite loop in comedi_cleanup
Removed infinite loop in comedi_free_board_minor
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 0.872127056122
Removed calls to 'mutex_destroy' (function is undefined)
Removed calls to 'put_device' (function is undefined)
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Removed calls to '__wake_up' (function is undefined)
Removed calls to 'kill_fasync' (function is undefined)
Removed calls to 'dev_warn' (function is undefined)
Defining function get_device as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Defining function __msecs_to_jiffies as symbolic
Removed calls to 'release_firmware' (function is undefined)
Defining function request_firmware as symbolic
Defining function __request_region as symbolic
Removed calls to 'free_irq' (function is undefined)
Removed calls to '__release_region' (function is undefined)
Removed calls to '_dev_info' (function is undefined)
Defining function printk as symbolic
Removed calls to '__mutex_init' (function is undefined)
Removed calls to '__init_rwsem' (function is undefined)
Removed calls to 'dev_err' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'down_write' (function is undefined)
Removed calls to 'up_write' (function is undefined)
Removed calls to 'device_destroy' (function is undefined)
Removed calls to 'vfree' (function is undefined)
Removed calls to 'vunmap' (function is undefined)
Defining function vzalloc as symbolic
Defining function vmalloc as symbolic
Defining function dma_alloc_attrs as symbolic
Defining function get_zeroed_page as symbolic
Defining function __phys_addr as symbolic
Defining function vmap as symbolic
Removed calls to 'dma_free_attrs' (function is undefined)
Removed calls to 'free_pages' (function is undefined)
Defining function device_create as symbolic
Defining function noop_llseek as symbolic
Removed calls to 'down_read' (function is undefined)
Removed calls to '__dynamic_dev_dbg' (function is undefined)
Removed calls to 'add_wait_queue' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'remove_wait_queue' (function is undefined)
Removed calls to 'up_read' (function is undefined)
Removed calls to '__might_fault' (function is undefined)
Removed calls to '__dynamic_pr_debug' (function is undefined)
Defining function fasync_helper as symbolic
Defining function capable as symbolic
Defining function down_read_trylock as symbolic
Defining function remap_pfn_range as symbolic
Defining function compat_alloc_user_space as symbolic
Removed calls to '__copy_from_user_overflow' (function is undefined)
Removed calls to 'do_gettimeofday' (function is undefined)
Removed calls to '__udelay' (function is undefined)
Removed calls to '__copy_to_user_overflow' (function is undefined)
Defining function _copy_to_user as symbolic
Defining function _copy_from_user as symbolic
Defining function memdup_user as symbolic
Defining function strlcpy as symbolic
Defining function default_wake_function as symbolic
Defining function kstrtouint as symbolic
Defining function snprintf as symbolic
Defining function seq_lseek as symbolic
Defining function seq_read as symbolic
Defining function single_release as symbolic
Defining function single_open as symbolic
Defining function seq_printf as symbolic
Defining function seq_puts as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'class_destroy' (function is undefined)
Removed calls to 'cdev_del' (function is undefined)
Removed calls to 'unregister_chrdev_region' (function is undefined)
Removed calls to 'remove_proc_entry' (function is undefined)
Removed calls to 'cdev_init' (function is undefined)
Defining function register_chrdev_region as symbolic
Defining function kobject_set_name as symbolic
Defining function cdev_add as symbolic
Defining function __class_create as symbolic
Defining function proc_create_data 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.817271947861
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 355 191 1333 10813
INFO: Starting verification
KLEE: WARNING ONCE: function "comedi_dev_put" has inline asm
KLEE: WARNING ONCE: function "comedi_dev_get_from_minor" has inline asm
KLEE: WARNING ONCE: function "comedi_dev_get" has inline asm
KLEE: WARNING ONCE: function "comedi_timeout" has inline asm
KLEE: WARNING ONCE: function "comedi_free_subdevice_minor" has inline asm
KLEE: WARNING ONCE: function "comedi_buf_map_put" has inline asm
KLEE: WARNING ONCE: function "comedi_buf_map_kref_release" has inline asm
KLEE: WARNING ONCE: function "comedi_buf_alloc" has inline asm
KLEE: WARNING ONCE: function "comedi_buf_write_alloc" has inline asm
KLEE: WARNING ONCE: function "comedi_buf_read_free" has inline asm
KLEE: WARNING ONCE: function "comedi_buf_write_samples" has inline asm
KLEE: WARNING ONCE: function "comedi_buf_read_samples" has inline asm
KLEE: WARNING ONCE: function "comedi_buf_map_get" has inline asm
KLEE: WARNING ONCE: function "comedi_read" has inline asm
KLEE: WARNING ONCE: function "comedi_write" has inline asm
KLEE: WARNING ONCE: function "comedi_poll" has inline asm
KLEE: WARNING ONCE: function "comedi_unlocked_ioctl" has inline asm
KLEE: WARNING ONCE: function "comedi_compat_ioctl" has inline asm
KLEE: WARNING ONCE: function "comedi_subdevice_from_minor" has inline asm
KLEE: WARNING ONCE: function "get_compat_cmd" has inline asm
KLEE: WARNING ONCE: function "put_compat_cmd" has inline asm
KLEE: WARNING ONCE: function "get_compat_insn" 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_57306337-248c-4f9a-84aa-18ce377fa9c1/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-jF4rGq/linux-4.2-rc1.tar.xz-08_1a-drivers--staging--comedi--comedi.ko-entry_point_false-unreach-call.cil.out.c:8508: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 8824 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 11112 states (over memory cap)
KLEE: WARNING: killing 11294 states (over memory cap)
KLEE: WARNING: killing 11055 states (over memory cap)
KLEE: WARNING: killing 11030 states (over memory cap)
KLEE: WARNING: killing 11076 states (over memory cap)
KLEE: WARNING: killing 10633 states (over memory cap)
KLEE: WARNING: killing 11164 states (over memory cap)
KLEE: WARNING: killing 10999 states (over memory cap)
KLEE: WARNING: killing 11735 states (over memory cap)
KLEE: WARNING: killing 11780 states (over memory cap)
KLEE: WARNING: killing 12235 states (over memory cap)
KLEE: WARNING: killing 12282 states (over memory cap)
KLEE: WARNING: killing 12403 states (over memory cap)
KLEE: WARNING: killing 12590 states (over memory cap)
KLEE: WARNING: killing 13052 states (over memory cap)
KLEE: WARNING: killing 13242 states (over memory cap)
KLEE: WARNING: killing 13088 states (over memory cap)
KLEE: WARNING: killing 12934 states (over memory cap)
KLEE: WARNING: killing 12643 states (over memory cap)
KLEE: WARNING: killing 12628 states (over memory cap)
KLEE: WARNING: killing 12546 states (over memory cap)
KLEE: WARNING: killing 12665 states (over memory cap)
KLEE: WARNING: killing 12375 states (over memory cap)
KLEE: WARNING: killing 12428 states (over memory cap)
KLEE: WARNING: killing 12203 states (over memory cap)
KLEE: WARNING: killing 11444 states (over memory cap)
KLEE: WARNING: killing 11899 states (over memory cap)
KLEE: WARNING: killing 12554 states (over memory cap)
KLEE: WARNING: killing 11796 states (over memory cap)
KLEE: WARNING: killing 12450 states (over memory cap)
KLEE: WARNING: killing 12164 states (over memory cap)
KLEE: WARNING: killing 12079 states (over memory cap)
KLEE: WARNING: killing 12196 states (over memory cap)
KLEE: WARNING: killing 12316 states (over memory cap)
KLEE: WARNING: killing 11834 states (over memory cap)
KLEE: WARNING: killing 12283 states (over memory cap)
KLEE: WARNING: killing 12732 states (over memory cap)
KLEE: WARNING: killing 12855 states (over memory cap)
KLEE: WARNING: killing 12239 states (over memory cap)
KLEE: WARNING: killing 12293 states (over memory cap)
KLEE: WARNING: killing 12144 states (over memory cap)
KLEE: WARNING: killing 12263 states (over memory cap)
KLEE: WARNING: killing 12054 states (over memory cap)
KLEE: WARNING: killing 12568 states (over memory cap)
KLEE: WARNING: killing 12289 states (over memory cap)
KLEE: WARNING: killing 12405 states (over memory cap)
KLEE: WARNING: killing 12255 states (over memory cap)
KLEE: WARNING: killing 11785 states (over memory cap)
KLEE: WARNING: killing 12296 states (over memory cap)
KLEE: WARNING: killing 12020 states (over memory cap)
KLEE: WARNING: killing 12265 states (over memory cap)
KLEE: WARNING: killing 12121 states (over memory cap)
KLEE: WARNING: killing 12304 states (over memory cap)
KLEE: WARNING: killing 12415 states (over memory cap)
KLEE: WARNING: killing 12663 states (over memory cap)
KLEE: WARNING: killing 12458 states (over memory cap)
KLEE: WARNING: killing 11992 states (over memory cap)
KLEE: WARNING: killing 12430 states (over memory cap)
KLEE: WARNING: killing 13001 states (over memory cap)
KLEE: WARNING: killing 12605 states (over memory cap)
KLEE: WARNING: killing 12200 states (over memory cap)
KLEE: WARNING: killing 11928 states (over memory cap)
KLEE: WARNING: killing 12826 states (over memory cap)
KLEE: WARNING: killing 12235 states (over memory cap)
KLEE: WARNING: killing 11767 states (over memory cap)
KLEE: WARNING: killing 11817 states (over memory cap)
KLEE: WARNING: killing 12055 states (over memory cap)
KLEE: WARNING: killing 12302 states (over memory cap)
KLEE: WARNING: killing 12350 states (over memory cap)
KLEE: WARNING: killing 12340 states (over memory cap)
KLEE: WARNING: killing 12066 states (over memory cap)
KLEE: WARNING: killing 12250 states (over memory cap)
KLEE: WARNING: killing 12175 states (over memory cap)
KLEE: WARNING: killing 12099 states (over memory cap)
KLEE: WARNING: killing 12282 states (over memory cap)
KLEE: WARNING: killing 12781 states (over memory cap)
KLEE: WARNING: killing 12578 states (over memory cap)
KLEE: WARNING: killing 12058 states (over memory cap)
KLEE: WARNING: killing 12361 states (over memory cap)
KLEE: WARNING: killing 12281 states (over memory cap)
KLEE: WARNING: killing 12396 states (over memory cap)
KLEE: WARNING: killing 12197 states (over memory cap)
KLEE: WARNING: killing 11990 states (over memory cap)
KLEE: WARNING: killing 12042 states (over memory cap)
KLEE: WARNING: killing 12537 states (over memory cap)
KLEE: WARNING: killing 12405 states (over memory cap)
KLEE: WARNING: killing 12072 states (over memory cap)
KLEE: WARNING: killing 12503 states (over memory cap)
KLEE: WARNING: killing 12367 states (over memory cap)
KLEE: WARNING: killing 12423 states (over memory cap)
KLEE: WARNING: killing 12407 states (over memory cap)
KLEE: WARNING: killing 12020 states (over memory cap)
KLEE: WARNING: killing 12320 states (over memory cap)
KLEE: WARNING: killing 12501 states (over memory cap)
KLEE: WARNING: killing 11923 states (over memory cap)
KLEE: WARNING: killing 12478 states (over memory cap)
KLEE: WARNING: killing 12402 states (over memory cap)
KLEE: WARNING: killing 12074 states (over memory cap)
KLEE: WARNING: killing 12318 states (over memory cap)
KLEE: WARNING: killing 12433 states (over memory cap)
KLEE: WARNING: killing 11860 states (over memory cap)
KLEE: WARNING: killing 12535 states (over memory cap)
KLEE: WARNING: killing 12205 states (over memory cap)
KLEE: WARNING: killing 12384 states (over memory cap)
KLEE: WARNING: killing 11877 states (over memory cap)
KLEE: WARNING: killing 12430 states (over memory cap)
KLEE: WARNING: killing 12229 states (over memory cap)
KLEE: WARNING: killing 11970 states (over memory cap)
KLEE: WARNING: killing 12452 states (over memory cap)
KLEE: WARNING: killing 11949 states (over memory cap)
KLEE: WARNING: killing 12375 states (over memory cap)
KLEE: WARNING: killing 11995 states (over memory cap)
KLEE: WARNING: killing 12227 states (over memory cap)
KLEE: WARNING: killing 12219 states (over memory cap)
KLEE: WARNING: killing 12152 states (over memory cap)
KLEE: WARNING: killing 12691 states (over memory cap)
KLEE: WARNING: killing 12438 states (over memory cap)
KLEE: WARNING: killing 12611 states (over memory cap)
KLEE: WARNING: killing 12233 states (over memory cap)
KLEE: WARNING: killing 11788 states (over memory cap)
KLEE: WARNING: killing 11899 states (over memory cap)
KLEE: WARNING: killing 12503 states (over memory cap)
KLEE: WARNING: killing 12682 states (over memory cap)
KLEE: WARNING: killing 12548 states (over memory cap)
KLEE: WARNING: killing 12356 states (over memory cap)
KLEE: WARNING: killing 12282 states (over memory cap)
KLEE: WARNING: killing 12455 states (over memory cap)
KLEE: WARNING: killing 12200 states (over memory cap)
KLEE: WARNING: killing 12377 states (over memory cap)
KLEE: WARNING: killing 12366 states (over memory cap)
KLEE: WARNING: killing 12358 states (over memory cap)
KLEE: WARNING: killing 12595 states (over memory cap)
KLEE: WARNING: killing 12096 states (over memory cap)
KLEE: WARNING: killing 12203 states (over memory cap)
KLEE: WARNING: killing 12071 states (over memory cap)
KLEE: WARNING: killing 12119 states (over memory cap)
KLEE: WARNING: killing 11750 states (over memory cap)
KLEE: WARNING: killing 11795 states (over memory cap)
KLEE: WARNING: killing 12207 states (over memory cap)
KLEE: WARNING: killing 12438 states (over memory cap)
KLEE: WARNING: killing 12672 states (over memory cap)
KLEE: WARNING: killing 12359 states (over memory cap)
KLEE: WARNING: killing 12414 states (over memory cap)
KLEE: WARNING: killing 12100 states (over memory cap)
KLEE: WARNING: killing 12696 states (over memory cap)
KLEE: WARNING: killing 12443 states (over memory cap)
KLEE: WARNING: killing 12436 states (over memory cap)
KLEE: WARNING: killing 12127 states (over memory cap)
KLEE: WARNING: killing 12115 states (over memory cap)
KLEE: WARNING: killing 12043 states (over memory cap)
KLEE: WARNING: killing 11908 states (over memory cap)
KLEE: WARNING: killing 11840 states (over memory cap)
KLEE: WARNING: killing 12544 states (over memory cap)
KLEE: WARNING: killing 12117 states (over memory cap)
KLEE: WARNING: killing 12642 states (over memory cap)
KLEE: WARNING: killing 12576 states (over memory cap)
KLEE: WARNING: killing 12087 states (over memory cap)
KLEE: WARNING: killing 12320 states (over memory cap)
KLEE: WARNING: killing 12429 states (over memory cap)
KLEE: WARNING: killing 12177 states (over memory cap)
KLEE: WARNING: killing 11990 states (over memory cap)
KLEE: WARNING: killing 12099 states (over memory cap)
KLEE: WARNING: killing 12325 states (over memory cap)
KLEE: WARNING: killing 12193 states (over memory cap)
KLEE: WARNING: killing 11947 states (over memory cap)
KLEE: WARNING: killing 12472 states (over memory cap)
KLEE: WARNING: killing 12517 states (over memory cap)
KLEE: WARNING: killing 11981 states (over memory cap)
KLEE: WARNING: killing 12323 states (over memory cap)
KLEE: WARNING: killing 11486 states (over memory cap)
KLEE: WARNING: killing 12416 states (over memory cap)
KLEE: WARNING: killing 12173 states (over memory cap)
KLEE: WARNING: killing 12281 states (over memory cap)
KLEE: WARNING: killing 12448 states (over memory cap)
KLEE: WARNING: killing 12319 states (over memory cap)
KLEE: WARNING: killing 12545 states (over memory cap)
KLEE: WARNING: killing 12357 states (over memory cap)
KLEE: WARNING: killing 11997 states (over memory cap)
KLEE: WARNING: killing 12572 states (over memory cap)
KLEE: WARNING: killing 12035 states (over memory cap)
KLEE: WARNING: killing 12552 states (over memory cap)
KLEE: WARNING: killing 12304 states (over memory cap)
KLEE: WARNING: killing 12116 states (over memory cap)
KLEE: WARNING: killing 12577 states (over memory cap)
KLEE: WARNING: killing 12683 states (over memory cap)
KLEE: WARNING: killing 11858 states (over memory cap)
KLEE: WARNING: killing 12136 states (over memory cap)
