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--usb--serial--ti_usb_3410_5052.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.: 134 134 1438 7985
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.339447975159
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'dev_err' (function is undefined)
Removed calls to 'release_firmware' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'usb_kill_urb' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to '__might_fault' (function is undefined)
Removed calls to 'tty_encode_baud_rate' (function is undefined)
Defining function usb_serial_generic_tiocmiwait as symbolic
Defining function usb_serial_generic_get_icount as symbolic
Removed calls to '__wake_up' (function is undefined)
Removed calls to 'tty_wakeup' (function is undefined)
Removed calls to 'tty_kref_put' (function is undefined)
Removed calls to 'tty_flip_buffer_push' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'tty_port_tty_wakeup' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Defining function __kfifo_out as symbolic
Defining function usb_submit_urb as symbolic
Defining function tty_insert_flip_string_fixed_flag as symbolic
Defining function tty_port_tty_get as symbolic
Defining function usb_control_msg as symbolic
Defining function tty_termios_baud_rate as symbolic
Defining function __msecs_to_jiffies as symbolic
Defining function _copy_from_user as symbolic
Defining function jiffies_to_msecs as symbolic
Defining function _copy_to_user as symbolic
Defining function __kfifo_in as symbolic
Removed calls to 'mutex_unlock' (function is undefined)
Defining function mutex_lock_interruptible as symbolic
Defining function usb_clear_halt as symbolic
Defining function msleep_interruptible as symbolic
Defining function usb_reset_device as symbolic
Defining function usb_driver_set_configuration as symbolic
Defining function sprintf as symbolic
Defining function request_firmware as symbolic
Defining function usb_bulk_msg as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'usb_serial_deregister_drivers' (function is undefined)
Defining function ldv_detach_1 as symbolic
Defining function ldv_probe_1 as symbolic
Defining function ldv_detach_2 as symbolic
Defining function ldv_probe_2 as symbolic
Defining function usb_serial_register_drivers as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Defining function mutex_trylock as symbolic
Linked our definitions to these undefined functions:
  strcpy
  __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.335474967957
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 153 136 744 4867
INFO: Starting verification
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_708abfe5-63b9-40fe-a74e-9b3dc721de4c/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-U8ngoH/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--serial--ti_usb_3410_5052.ko-entry_point_true-unreach-call.cil.out.c:5320: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-U8ngoH/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--serial--ti_usb_3410_5052.ko-entry_point_true-unreach-call.cil.out.c:5643: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-U8ngoH/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--serial--ti_usb_3410_5052.ko-entry_point_true-unreach-call.cil.out.c:5277: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-U8ngoH/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--serial--ti_usb_3410_5052.ko-entry_point_true-unreach-call.cil.out.c:5296: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-U8ngoH/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--serial--ti_usb_3410_5052.ko-entry_point_true-unreach-call.cil.out.c:5701: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-U8ngoH/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--serial--ti_usb_3410_5052.ko-entry_point_true-unreach-call.cil.out.c:5910: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-U8ngoH/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--serial--ti_usb_3410_5052.ko-entry_point_true-unreach-call.cil.out.c:5602: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-U8ngoH/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--serial--ti_usb_3410_5052.ko-entry_point_true-unreach-call.cil.out.c:5182: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-U8ngoH/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--serial--ti_usb_3410_5052.ko-entry_point_true-unreach-call.cil.out.c:5355: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-U8ngoH/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--serial--ti_usb_3410_5052.ko-entry_point_true-unreach-call.cil.out.c:5240: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-U8ngoH/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--serial--ti_usb_3410_5052.ko-entry_point_true-unreach-call.cil.out.c:4722: 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 7822 states (over memory cap)
KLEE: WARNING: killing 11969 states (over memory cap)
KLEE: WARNING: killing 12738 states (over memory cap)
KLEE: WARNING: killing 12618 states (over memory cap)
KLEE: WARNING: killing 12640 states (over memory cap)
KLEE: WARNING: killing 7278 states (over memory cap)
KLEE: WARNING: killing 14279 states (over memory cap)
KLEE: WARNING: killing 7722 states (over memory cap)
KLEE: WARNING: killing 6775 states (over memory cap)
KLEE: WARNING: killing 6899 states (over memory cap)
KLEE: WARNING: killing 6754 states (over memory cap)
KLEE: WARNING: killing 7147 states (over memory cap)
KLEE: WARNING: killing 12945 states (over memory cap)
KLEE: WARNING: killing 7791 states (over memory cap)
KLEE: WARNING: killing 7047 states (over memory cap)
KLEE: WARNING: killing 6838 states (over memory cap)
KLEE: WARNING: killing 7030 states (over memory cap)
KLEE: WARNING: killing 6885 states (over memory cap)
KLEE: WARNING: killing 13571 states (over memory cap)
KLEE: WARNING: killing 7192 states (over memory cap)
KLEE: WARNING: killing 7316 states (over memory cap)
KLEE: WARNING: killing 6841 states (over memory cap)
KLEE: WARNING: killing 6831 states (over memory cap)
KLEE: WARNING: killing 6756 states (over memory cap)
KLEE: WARNING: killing 7210 states (over memory cap)
KLEE: WARNING: killing 7069 states (over memory cap)
KLEE: WARNING: killing 6863 states (over memory cap)
KLEE: WARNING: killing 6852 states (over memory cap)
KLEE: WARNING: killing 7435 states (over memory cap)
KLEE: WARNING: killing 7622 states (over memory cap)
KLEE: WARNING: killing 7290 states (over memory cap)
KLEE: WARNING: killing 7542 states (over memory cap)
KLEE: WARNING: killing 7995 states (over memory cap)
KLEE: WARNING: killing 7925 states (over memory cap)
KLEE: WARNING: killing 7336 states (over memory cap)
KLEE: WARNING: killing 7847 states (over memory cap)
KLEE: WARNING: killing 7645 states (over memory cap)
KLEE: WARNING: killing 8291 states (over memory cap)
KLEE: WARNING: killing 8028 states (over memory cap)
KLEE: WARNING: killing 7438 states (over memory cap)
KLEE: WARNING: killing 7886 states (over memory cap)
KLEE: WARNING: killing 8271 states (over memory cap)
KLEE: WARNING: killing 7679 states (over memory cap)
KLEE: WARNING: killing 7996 states (over memory cap)
KLEE: WARNING: killing 8252 states (over memory cap)
KLEE: WARNING: killing 8374 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-U8ngoH/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--serial--ti_usb_3410_5052.ko-entry_point_true-unreach-call.cil.out.c:4659: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 7201 states (over memory cap)
KLEE: WARNING: killing 7453 states (over memory cap)
KLEE: WARNING: killing 8475 states (over memory cap)
KLEE: WARNING: killing 7243 states (over memory cap)
KLEE: WARNING: killing 8009 states (over memory cap)
KLEE: WARNING: killing 7615 states (over memory cap)
KLEE: WARNING: killing 7413 states (over memory cap)
KLEE: WARNING: killing 7468 states (over memory cap)
KLEE: WARNING: killing 7073 states (over memory cap)
KLEE: WARNING: killing 7450 states (over memory cap)
KLEE: WARNING: killing 7568 states (over memory cap)
KLEE: WARNING: killing 7751 states (over memory cap)
KLEE: WARNING: killing 7427 states (over memory cap)
KLEE: WARNING: killing 8122 states (over memory cap)
KLEE: WARNING: killing 7605 states (over memory cap)
KLEE: WARNING: killing 7153 states (over memory cap)
KLEE: WARNING: killing 7080 states (over memory cap)
KLEE: WARNING: killing 7833 states (over memory cap)
KLEE: WARNING: killing 7250 states (over memory cap)
KLEE: WARNING: killing 7181 states (over memory cap)
KLEE: WARNING: killing 6985 states (over memory cap)
KLEE: WARNING: killing 7606 states (over memory cap)
KLEE: WARNING: killing 7094 states (over memory cap)
KLEE: WARNING: killing 6645 states (over memory cap)
KLEE: WARNING: killing 7329 states (over memory cap)
KLEE: WARNING: killing 7890 states (over memory cap)
KLEE: WARNING: killing 7822 states (over memory cap)
KLEE: WARNING: killing 7248 states (over memory cap)
KLEE: WARNING: killing 7432 states (over memory cap)
KLEE: WARNING: killing 7610 states (over memory cap)
KLEE: WARNING: killing 7164 states (over memory cap)
KLEE: WARNING: killing 7661 states (over memory cap)
KLEE: WARNING: killing 7717 states (over memory cap)
KLEE: WARNING: killing 7148 states (over memory cap)
KLEE: WARNING: killing 7955 states (over memory cap)
KLEE: WARNING: killing 7384 states (over memory cap)
KLEE: WARNING: killing 7378 states (over memory cap)
KLEE: WARNING: killing 7369 states (over memory cap)
KLEE: WARNING: killing 7612 states (over memory cap)
KLEE: WARNING: killing 8291 states (over memory cap)
KLEE: WARNING: killing 7976 states (over memory cap)
KLEE: WARNING: killing 8032 states (over memory cap)
KLEE: WARNING: killing 7784 states (over memory cap)
KLEE: WARNING: killing 7966 states (over memory cap)
KLEE: WARNING: killing 6779 states (over memory cap)
KLEE: WARNING: killing 7830 states (over memory cap)
KLEE: WARNING: killing 7513 states (over memory cap)
KLEE: WARNING: killing 7690 states (over memory cap)
KLEE: WARNING: killing 7375 states (over memory cap)
KLEE: WARNING: killing 7679 states (over memory cap)
KLEE: WARNING: killing 7298 states (over memory cap)
KLEE: WARNING: killing 7786 states (over memory cap)
KLEE: WARNING: killing 6851 states (over memory cap)
KLEE: WARNING: killing 7213 states (over memory cap)
KLEE: WARNING: killing 7697 states (over memory cap)
KLEE: WARNING: killing 7263 states (over memory cap)
KLEE: WARNING: killing 6822 states (over memory cap)
KLEE: WARNING: killing 7676 states (over memory cap)
KLEE: WARNING: killing 7608 states (over memory cap)
KLEE: WARNING: killing 7661 states (over memory cap)
KLEE: WARNING: killing 8454 states (over memory cap)
KLEE: WARNING: killing 8022 states (over memory cap)
KLEE: WARNING: killing 7775 states (over memory cap)
KLEE: WARNING: killing 7953 states (over memory cap)
KLEE: WARNING: killing 7642 states (over memory cap)
KLEE: WARNING: killing 7207 states (over memory cap)
KLEE: WARNING: killing 7749 states (over memory cap)
KLEE: WARNING: killing 7013 states (over memory cap)
KLEE: WARNING: killing 7490 states (over memory cap)
KLEE: WARNING: killing 6876 states (over memory cap)
KLEE: WARNING: killing 7959 states (over memory cap)
KLEE: WARNING: killing 7045 states (over memory cap)
KLEE: WARNING: killing 6974 states (over memory cap)
KLEE: WARNING: killing 7395 states (over memory cap)
KLEE: WARNING: killing 8051 states (over memory cap)
KLEE: WARNING: killing 7804 states (over memory cap)
KLEE: WARNING: killing 7683 states (over memory cap)
KLEE: WARNING: killing 7919 states (over memory cap)
KLEE: WARNING: killing 7249 states (over memory cap)
KLEE: WARNING: killing 7421 states (over memory cap)
KLEE: WARNING: killing 7355 states (over memory cap)
KLEE: WARNING: killing 7411 states (over memory cap)
KLEE: WARNING: killing 7706 states (over memory cap)
KLEE: WARNING: killing 7397 states (over memory cap)
KLEE: WARNING: killing 7330 states (over memory cap)
KLEE: WARNING: killing 7444 states (over memory cap)
KLEE: WARNING: killing 7801 states (over memory cap)
KLEE: WARNING: killing 7313 states (over memory cap)
KLEE: WARNING: killing 7247 states (over memory cap)
KLEE: WARNING: killing 7719 states (over memory cap)
KLEE: WARNING: killing 7775 states (over memory cap)
KLEE: WARNING: killing 7892 states (over memory cap)
KLEE: WARNING: killing 7767 states (over memory cap)
KLEE: WARNING: killing 7704 states (over memory cap)
KLEE: WARNING: killing 7698 states (over memory cap)
KLEE: WARNING: killing 7096 states (over memory cap)
KLEE: WARNING: killing 7270 states (over memory cap)
KLEE: WARNING: killing 7978 states (over memory cap)
KLEE: WARNING: killing 7855 states (over memory cap)
KLEE: WARNING: killing 7911 states (over memory cap)
KLEE: WARNING: killing 7015 states (over memory cap)
KLEE: WARNING: killing 7601 states (over memory cap)
KLEE: WARNING: killing 7003 states (over memory cap)
KLEE: WARNING: killing 7765 states (over memory cap)
KLEE: WARNING: killing 8116 states (over memory cap)
KLEE: WARNING: killing 7339 states (over memory cap)
KLEE: WARNING: killing 6977 states (over memory cap)
KLEE: WARNING: killing 7501 states (over memory cap)
KLEE: WARNING: killing 7497 states (over memory cap)
KLEE: WARNING: killing 7489 states (over memory cap)
KLEE: WARNING: killing 7188 states (over memory cap)
KLEE: WARNING: killing 7476 states (over memory cap)
KLEE: WARNING: killing 7119 states (over memory cap)
KLEE: WARNING: killing 7582 states (over memory cap)
KLEE: WARNING: killing 7458 states (over memory cap)
KLEE: WARNING: killing 6688 states (over memory cap)
KLEE: WARNING: killing 7620 states (over memory cap)
KLEE: WARNING: killing 7202 states (over memory cap)
KLEE: WARNING: killing 7309 states (over memory cap)
KLEE: WARNING: killing 7600 states (over memory cap)
KLEE: WARNING: killing 7067 states (over memory cap)
KLEE: WARNING: killing 7175 states (over memory cap)
KLEE: WARNING: killing 7287 states (over memory cap)
KLEE: WARNING: killing 7865 states (over memory cap)
KLEE: WARNING: killing 7453 states (over memory cap)
KLEE: WARNING: killing 7328 states (over memory cap)
KLEE: WARNING: killing 7267 states (over memory cap)
KLEE: WARNING: killing 6972 states (over memory cap)
KLEE: WARNING: killing 7549 states (over memory cap)
KLEE: WARNING: killing 7254 states (over memory cap)
KLEE: WARNING: killing 7774 states (over memory cap)
KLEE: WARNING: killing 7825 states (over memory cap)
KLEE: WARNING: killing 7362 states (over memory cap)
KLEE: WARNING: killing 7704 states (over memory cap)
KLEE: WARNING: killing 7585 states (over memory cap)
KLEE: WARNING: killing 7289 states (over memory cap)
KLEE: WARNING: killing 7109 states (over memory cap)
KLEE: WARNING: killing 7333 states (over memory cap)
KLEE: WARNING: killing 7040 states (over memory cap)
KLEE: WARNING: killing 7614 states (over memory cap)
KLEE: WARNING: killing 7605 states (over memory cap)
KLEE: WARNING: killing 7662 states (over memory cap)
KLEE: WARNING: killing 7427 states (over memory cap)
