bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.12-rc1/linux-3.12-rc1.tar.xz-08_1a-drivers--staging--comedi--comedi.ko-entry_point_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.: 176 226 2785 17501
Removed infinite loop in comedi_dev_from_board_minor
Removed infinite loop in comedi_subdevice_from_minor
Removed infinite loop in arch_local_save_flags
Removed infinite loop in comedi_free_subdevice_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.691226959229
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function noop_llseek as symbolic
Removed calls to 'add_wait_queue' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'might_fault' (function is undefined)
Removed calls to 'remove_wait_queue' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Defining function fasync_helper as symbolic
Defining function dev_err as symbolic
Defining function _raw_spin_lock_irqsave as symbolic
Defining function capable as symbolic
Defining function __phys_addr as symbolic
Defining function remap_pfn_range as symbolic
Defining function compat_alloc_user_space as symbolic
Removed calls to 'device_destroy' (function is undefined)
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Removed calls to 'do_gettimeofday' (function is undefined)
Removed calls to '__udelay' (function is undefined)
Defining function _copy_to_user as symbolic
Defining function printk as symbolic
Defining function dev_warn as symbolic
Defining function _copy_from_user as symbolic
Defining function strlcpy as symbolic
Removed calls to 'debug_dma_alloc_coherent' (function is undefined)
Removed calls to 'vfree' (function is undefined)
Removed calls to 'vunmap' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'debug_dma_free_coherent' (function is undefined)
Removed calls to 'free_pages' (function is undefined)
Defining function vzalloc as symbolic
Defining function vmalloc as symbolic
Defining function get_zeroed_page as symbolic
Defining function vmap as symbolic
Removed calls to 'mutex_destroy' (function is undefined)
Removed calls to 'put_device' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Defining function device_create 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 'kill_fasync' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Defining function get_device 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)
Defining function register_chrdev_region as symbolic
Removed calls to 'cdev_init' (function is undefined)
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
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 'pci_disable_device' (function is undefined)
Defining function pci_enable_device as symbolic
Defining function pci_request_regions as symbolic
Removed calls to 'pci_release_regions' (function is undefined)
Defining function __pci_register_driver as symbolic
Removed calls to 'pci_unregister_driver' (function is undefined)
Defining function pcmcia_loop_config as symbolic
Defining function pcmcia_enable_device as symbolic
Defining function pcmcia_request_io as symbolic
Removed calls to 'pcmcia_disable_device' (function is undefined)
Defining function pcmcia_register_driver as symbolic
Removed calls to 'pcmcia_unregister_driver' (function is undefined)
Defining function usb_register_driver as symbolic
Removed calls to 'usb_deregister' (function is undefined)
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_loff_t_named
  __VERIFIER_nondet_pointer_named
  __VERIFIER_nondet_size_t_named
  __VERIFIER_nondet_uint_named
  __VERIFIER_nondet_ulong_named
INFO: After-slicing optimizations and preparation time: 0.650985002518
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 286 199 1337 9511
INFO: Starting verification
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 "get_compat_insn" has inline asm
KLEE: WARNING ONCE: function "comedi_buf_alloc" has inline asm
KLEE: WARNING ONCE: function "__comedi_buf_free" has inline asm
KLEE: WARNING ONCE: function "comedi_free_subdevice_minor" has inline asm
KLEE: WARNING ONCE: function "comedi_buf_read_free" has inline asm
KLEE: WARNING ONCE: function "comedi_buf_write_alloc" has inline asm
KLEE: WARNING ONCE: function "main" has inline asm
KLEE: WARNING ONCE: function "comedi_buf_put" has inline asm
KLEE: WARNING ONCE: function "comedi_buf_get" 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_9f94c2a1-b64e-4257-acb6-dedcfe304a31/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 7973 states (over memory cap)
KLEE: WARNING: killing 7232 states (over memory cap)
KLEE: WARNING: killing 7594 states (over memory cap)
KLEE: WARNING: killing 7486 states (over memory cap)
KLEE: WARNING: killing 8060 states (over memory cap)
KLEE: WARNING: killing 8213 states (over memory cap)
KLEE: WARNING: killing 8681 states (over memory cap)
KLEE: WARNING: killing 9363 states (over memory cap)
KLEE: WARNING: killing 9147 states (over memory cap)
KLEE: WARNING: killing 10507 states (over memory cap)
KLEE: WARNING: killing 10608 states (over memory cap)
KLEE: WARNING: killing 10972 states (over memory cap)
KLEE: WARNING: killing 11808 states (over memory cap)
KLEE: WARNING: killing 12116 states (over memory cap)
KLEE: WARNING: killing 11791 states (over memory cap)
KLEE: WARNING: killing 12093 states (over memory cap)
KLEE: WARNING: killing 12394 states (over memory cap)
KLEE: WARNING: killing 12543 states (over memory cap)
KLEE: WARNING: killing 12368 states (over memory cap)
KLEE: WARNING: killing 12615 states (over memory cap)
KLEE: WARNING: killing 12179 states (over memory cap)
KLEE: WARNING: killing 12842 states (over memory cap)
KLEE: WARNING: killing 12723 states (over memory cap)
KLEE: WARNING: killing 12651 states (over memory cap)
KLEE: WARNING: killing 13159 states (over memory cap)
KLEE: WARNING: killing 13093 states (over memory cap)
KLEE: WARNING: killing 12810 states (over memory cap)
KLEE: WARNING: killing 13315 states (over memory cap)
KLEE: WARNING: killing 12723 states (over memory cap)
KLEE: WARNING: killing 12863 states (over memory cap)
KLEE: WARNING: killing 12692 states (over memory cap)
KLEE: WARNING: killing 13395 states (over memory cap)
KLEE: WARNING: killing 12819 states (over memory cap)
KLEE: WARNING: killing 12802 states (over memory cap)
KLEE: WARNING: killing 13095 states (over memory cap)
KLEE: WARNING: killing 12562 states (over memory cap)
KLEE: WARNING: killing 12290 states (over memory cap)
KLEE: WARNING: killing 13195 states (over memory cap)
KLEE: WARNING: killing 12876 states (over memory cap)
KLEE: WARNING: killing 12500 states (over memory cap)
KLEE: WARNING: killing 12844 states (over memory cap)
KLEE: WARNING: killing 12366 states (over memory cap)
KLEE: WARNING: killing 13120 states (over memory cap)
KLEE: WARNING: killing 12700 states (over memory cap)
KLEE: WARNING: killing 12687 states (over memory cap)
KLEE: WARNING: killing 13028 states (over memory cap)
KLEE: WARNING: killing 12864 states (over memory cap)
KLEE: WARNING: killing 12848 states (over memory cap)
KLEE: WARNING: killing 12481 states (over memory cap)
KLEE: WARNING: killing 12617 states (over memory cap)
KLEE: WARNING: killing 12704 states (over memory cap)
KLEE: WARNING: killing 12889 states (over memory cap)
KLEE: WARNING: killing 12526 states (over memory cap)
KLEE: WARNING: killing 13063 states (over memory cap)
KLEE: WARNING: killing 12647 states (over memory cap)
KLEE: WARNING: killing 12934 states (over memory cap)
KLEE: WARNING: killing 13428 states (over memory cap)
KLEE: WARNING: killing 12260 states (over memory cap)
KLEE: WARNING: killing 12602 states (over memory cap)
KLEE: WARNING: killing 12686 states (over memory cap)
KLEE: WARNING: killing 13127 states (over memory cap)
KLEE: WARNING: killing 12864 states (over memory cap)
KLEE: WARNING: killing 13098 states (over memory cap)
KLEE: WARNING: killing 12691 states (over memory cap)
KLEE: WARNING: killing 12428 states (over memory cap)
KLEE: WARNING: killing 12812 states (over memory cap)
KLEE: WARNING: killing 12101 states (over memory cap)
KLEE: WARNING: killing 13283 states (over memory cap)
KLEE: WARNING: killing 12524 states (over memory cap)
KLEE: WARNING: killing 12662 states (over memory cap)
KLEE: WARNING: killing 13195 states (over memory cap)
KLEE: WARNING: killing 12337 states (over memory cap)
KLEE: WARNING: killing 13019 states (over memory cap)
KLEE: WARNING: killing 12461 states (over memory cap)
KLEE: WARNING: killing 12843 states (over memory cap)
KLEE: WARNING: killing 12983 states (over memory cap)
KLEE: WARNING: killing 12872 states (over memory cap)
KLEE: WARNING: killing 13155 states (over memory cap)
KLEE: WARNING: killing 12800 states (over memory cap)
KLEE: WARNING: killing 12697 states (over memory cap)
KLEE: WARNING: killing 12973 states (over memory cap)
KLEE: WARNING: killing 12374 states (over memory cap)
KLEE: WARNING: killing 12848 states (over memory cap)
KLEE: WARNING: killing 12398 states (over memory cap)
KLEE: WARNING: killing 12776 states (over memory cap)
KLEE: WARNING: killing 12716 states (over memory cap)
KLEE: WARNING: killing 12703 states (over memory cap)
KLEE: WARNING: killing 12837 states (over memory cap)
KLEE: WARNING: killing 12634 states (over memory cap)
KLEE: WARNING: killing 12666 states (over memory cap)
KLEE: WARNING: killing 13192 states (over memory cap)
KLEE: WARNING: killing 12740 states (over memory cap)
KLEE: WARNING: killing 12978 states (over memory cap)
KLEE: WARNING: killing 12774 states (over memory cap)
KLEE: WARNING: killing 12714 states (over memory cap)
KLEE: WARNING: killing 13189 states (over memory cap)
KLEE: WARNING: killing 12498 states (over memory cap)
KLEE: WARNING: killing 12485 states (over memory cap)
KLEE: WARNING: killing 12956 states (over memory cap)
KLEE: WARNING: killing 12945 states (over memory cap)
KLEE: WARNING: killing 12693 states (over memory cap)
KLEE: WARNING: killing 13167 states (over memory cap)
KLEE: WARNING: killing 12772 states (over memory cap)
KLEE: WARNING: killing 12614 states (over memory cap)
KLEE: WARNING: killing 12698 states (over memory cap)
KLEE: WARNING: killing 13654 states (over memory cap)
KLEE: WARNING: killing 13261 states (over memory cap)
KLEE: WARNING: killing 12579 states (over memory cap)
KLEE: WARNING: killing 12613 states (over memory cap)
KLEE: WARNING: killing 12892 states (over memory cap)
KLEE: WARNING: killing 12877 states (over memory cap)
KLEE: WARNING: killing 12197 states (over memory cap)
KLEE: WARNING: killing 12470 states (over memory cap)
KLEE: WARNING: killing 12412 states (over memory cap)
KLEE: WARNING: killing 12731 states (over memory cap)
KLEE: WARNING: killing 12767 states (over memory cap)
KLEE: WARNING: killing 12470 states (over memory cap)
KLEE: WARNING: killing 12889 states (over memory cap)
KLEE: WARNING: killing 13355 states (over memory cap)
KLEE: WARNING: killing 12827 states (over memory cap)
KLEE: WARNING: killing 12577 states (over memory cap)
KLEE: WARNING: killing 12903 states (over memory cap)
KLEE: WARNING: killing 13124 states (over memory cap)
KLEE: WARNING: killing 12920 states (over memory cap)
KLEE: WARNING: killing 12913 states (over memory cap)
KLEE: WARNING: killing 12760 states (over memory cap)
KLEE: WARNING: killing 12607 states (over memory cap)
KLEE: WARNING: killing 12541 states (over memory cap)
KLEE: WARNING: killing 12810 states (over memory cap)
KLEE: WARNING: killing 12516 states (over memory cap)
KLEE: WARNING: killing 12838 states (over memory cap)
KLEE: WARNING: killing 12827 states (over memory cap)
KLEE: WARNING: killing 12438 states (over memory cap)
KLEE: WARNING: killing 12899 states (over memory cap)
