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-43_2a-drivers--usb--serial--io_edgeport.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.: 273 127 2423 16048
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.50381398201
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to '_dev_info' (function is undefined)
Removed calls to 'dev_err' (function is undefined)
Removed calls to 'dev_warn' (function is undefined)
Removed calls to 'release_firmware' (function is undefined)
Removed calls to 'usb_free_urb' (function is undefined)
Removed calls to 'usb_kill_urb' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to 'prepare_to_wait' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function usb_serial_generic_tiocmiwait as symbolic
Defining function usb_serial_generic_get_icount as symbolic
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)
Removed calls to '__wake_up' (function is undefined)
Removed calls to 'tty_kref_put' (function is undefined)
Removed calls to 'tty_flip_buffer_push' (function is undefined)
Defining function tty_insert_flip_string_fixed_flag as symbolic
Defining function tty_port_tty_get as symbolic
Removed calls to 'tty_encode_baud_rate' (function is undefined)
Defining function tty_termios_baud_rate as symbolic
Defining function autoremove_wake_function as symbolic
Defining function schedule_timeout as symbolic
Removed calls to '__might_fault' (function is undefined)
Removed calls to '__copy_to_user_overflow' (function is undefined)
Defining function _copy_to_user as symbolic
Defining function prepare_to_wait_event as symbolic
Defining function usb_string as symbolic
Defining function usb_control_msg as symbolic
Defining function request_firmware as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'usb_serial_deregister_drivers' (function is undefined)
Removed calls to 'ldv_check_final_state' (function is undefined)
Defining function ldv_probe_4 as symbolic
Defining function ldv_probe_1 as symbolic
Defining function ldv_probe_3 as symbolic
Defining function ldv_probe_2 as symbolic
Defining function usb_serial_register_drivers as symbolic
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  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.531420946121
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 231 98 939 8465
INFO: Starting verification
KLEE: WARNING ONCE: function "edge_close" has inline asm
KLEE: WARNING ONCE: function "edge_ioctl" has inline asm
KLEE: WARNING ONCE: function "write_cmd_usb" has inline asm
KLEE: WARNING ONCE: function "edge_bulk_out_cmd_callback" has inline asm
KLEE: WARNING ONCE: function "block_until_chase_response" 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_ae2b9ddd-5252-4a4d-9372-e35bc21c8606/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 10151 states (over memory cap)
KLEE: WARNING: killing 7339 states (over memory cap)
KLEE: WARNING: killing 7069 states (over memory cap)
KLEE: WARNING: killing 7259 states (over memory cap)
KLEE: WARNING: killing 7044 states (over memory cap)
KLEE: WARNING: killing 7281 states (over memory cap)
KLEE: WARNING: killing 7571 states (over memory cap)
KLEE: WARNING: killing 7562 states (over memory cap)
KLEE: WARNING: killing 7348 states (over memory cap)
KLEE: WARNING: killing 7489 states (over memory cap)
KLEE: WARNING: killing 7478 states (over memory cap)
KLEE: WARNING: killing 7667 states (over memory cap)
KLEE: WARNING: killing 7956 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-B7GM5R/linux-4.2-rc1.tar.xz-43_2a-drivers--usb--serial--io_edgeport.ko-entry_point_true-unreach-call.cil.out.c:7107: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-B7GM5R/linux-4.2-rc1.tar.xz-43_2a-drivers--usb--serial--io_edgeport.ko-entry_point_true-unreach-call.cil.out.c:6917: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-B7GM5R/linux-4.2-rc1.tar.xz-43_2a-drivers--usb--serial--io_edgeport.ko-entry_point_true-unreach-call.cil.out.c:7270: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 8142 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-B7GM5R/linux-4.2-rc1.tar.xz-43_2a-drivers--usb--serial--io_edgeport.ko-entry_point_true-unreach-call.cil.out.c:7045: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-B7GM5R/linux-4.2-rc1.tar.xz-43_2a-drivers--usb--serial--io_edgeport.ko-entry_point_true-unreach-call.cil.out.c:4266: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-B7GM5R/linux-4.2-rc1.tar.xz-43_2a-drivers--usb--serial--io_edgeport.ko-entry_point_true-unreach-call.cil.out.c:6980: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-B7GM5R/linux-4.2-rc1.tar.xz-43_2a-drivers--usb--serial--io_edgeport.ko-entry_point_true-unreach-call.cil.out.c:5999: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 9128 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-B7GM5R/linux-4.2-rc1.tar.xz-43_2a-drivers--usb--serial--io_edgeport.ko-entry_point_true-unreach-call.cil.out.c:7438: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 8866 states (over memory cap)
KLEE: WARNING: killing 8451 states (over memory cap)
KLEE: WARNING: killing 8537 states (over memory cap)
KLEE: WARNING: killing 8228 states (over memory cap)
KLEE: WARNING: killing 8117 states (over memory cap)
KLEE: WARNING: killing 8695 states (over memory cap)
KLEE: WARNING: killing 8683 states (over memory cap)
KLEE: WARNING: killing 8326 states (over memory cap)
KLEE: WARNING: killing 8605 states (over memory cap)
KLEE: WARNING: killing 8743 states (over memory cap)
KLEE: WARNING: killing 9122 states (over memory cap)
KLEE: WARNING: killing 8716 states (over memory cap)
KLEE: WARNING: killing 8508 states (over memory cap)
KLEE: WARNING: killing 8548 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-B7GM5R/linux-4.2-rc1.tar.xz-43_2a-drivers--usb--serial--io_edgeport.ko-entry_point_true-unreach-call.cil.out.c:9750: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 8579 states (over memory cap)
KLEE: WARNING: killing 9005 states (over memory cap)
KLEE: WARNING: killing 9093 states (over memory cap)
KLEE: WARNING: killing 8787 states (over memory cap)
KLEE: WARNING: killing 9067 states (over memory cap)
KLEE: WARNING: killing 8574 states (over memory cap)
KLEE: WARNING: killing 8659 states (over memory cap)
KLEE: WARNING: killing 9180 states (over memory cap)
KLEE: WARNING: killing 8782 states (over memory cap)
KLEE: WARNING: killing 9198 states (over memory cap)
KLEE: WARNING: killing 9140 states (over memory cap)
KLEE: WARNING: killing 8887 states (over memory cap)
KLEE: WARNING: killing 8540 states (over memory cap)
KLEE: WARNING: killing 8962 states (over memory cap)
KLEE: WARNING: killing 8662 states (over memory cap)
KLEE: WARNING: killing 8935 states (over memory cap)
KLEE: WARNING: killing 9070 states (over memory cap)
KLEE: WARNING: killing 8919 states (over memory cap)
KLEE: WARNING: killing 9291 states (over memory cap)
KLEE: WARNING: killing 8805 states (over memory cap)
KLEE: WARNING: killing 8798 states (over memory cap)
KLEE: WARNING: killing 8975 states (over memory cap)
KLEE: WARNING: killing 8966 states (over memory cap)
KLEE: WARNING: killing 8622 states (over memory cap)
KLEE: WARNING: killing 9183 states (over memory cap)
KLEE: WARNING: killing 8463 states (over memory cap)
KLEE: WARNING: killing 9016 states (over memory cap)
KLEE: WARNING: killing 8766 states (over memory cap)
KLEE: WARNING: killing 8712 states (over memory cap)
KLEE: WARNING: killing 9031 states (over memory cap)
KLEE: WARNING: killing 8930 states (over memory cap)
KLEE: WARNING: killing 9202 states (over memory cap)
KLEE: WARNING: killing 9336 states (over memory cap)
KLEE: WARNING: killing 8621 states (over memory cap)
KLEE: WARNING: killing 8565 states (over memory cap)
KLEE: WARNING: killing 9165 states (over memory cap)
KLEE: WARNING: killing 9252 states (over memory cap)
KLEE: WARNING: killing 8869 states (over memory cap)
KLEE: WARNING: killing 8674 states (over memory cap)
KLEE: WARNING: killing 9413 states (over memory cap)
KLEE: WARNING: killing 8750 states (over memory cap)
KLEE: WARNING: killing 8788 states (over memory cap)
KLEE: WARNING: killing 8547 states (over memory cap)
KLEE: WARNING: killing 8864 states (over memory cap)
KLEE: WARNING: killing 9088 states (over memory cap)
KLEE: WARNING: killing 9124 states (over memory cap)
KLEE: WARNING: killing 9211 states (over memory cap)
KLEE: WARNING: killing 8969 states (over memory cap)
KLEE: WARNING: killing 8774 states (over memory cap)
KLEE: WARNING: killing 9045 states (over memory cap)
KLEE: WARNING: killing 9548 states (over memory cap)
KLEE: WARNING: killing 8800 states (over memory cap)
KLEE: WARNING: killing 8883 states (over memory cap)
KLEE: WARNING: killing 8926 states (over memory cap)
KLEE: WARNING: killing 9239 states (over memory cap)
KLEE: WARNING: killing 8681 states (over memory cap)
KLEE: WARNING: killing 8578 states (over memory cap)
KLEE: WARNING: killing 9071 states (over memory cap)
KLEE: WARNING: killing 8789 states (over memory cap)
KLEE: WARNING: killing 8782 states (over memory cap)
KLEE: WARNING: killing 8863 states (over memory cap)
KLEE: WARNING: killing 9086 states (over memory cap)
KLEE: WARNING: killing 8804 states (over memory cap)
KLEE: WARNING: killing 8517 states (over memory cap)
KLEE: WARNING: killing 8922 states (over memory cap)
KLEE: WARNING: killing 9141 states (over memory cap)
KLEE: WARNING: killing 8997 states (over memory cap)
KLEE: WARNING: killing 8992 states (over memory cap)
KLEE: WARNING: killing 8847 states (over memory cap)
KLEE: WARNING: killing 9430 states (over memory cap)
KLEE: WARNING: killing 8788 states (over memory cap)
KLEE: WARNING: killing 9003 states (over memory cap)
KLEE: WARNING: killing 9314 states (over memory cap)
KLEE: WARNING: killing 9307 states (over memory cap)
KLEE: WARNING: killing 9072 states (over memory cap)
KLEE: WARNING: killing 9016 states (over memory cap)
KLEE: WARNING: killing 8872 states (over memory cap)
KLEE: WARNING: killing 8821 states (over memory cap)
KLEE: WARNING: killing 9266 states (over memory cap)
KLEE: WARNING: killing 8756 states (over memory cap)
KLEE: WARNING: killing 8795 states (over memory cap)
KLEE: WARNING: killing 9056 states (over memory cap)
KLEE: WARNING: killing 9455 states (over memory cap)
KLEE: WARNING: killing 8639 states (over memory cap)
KLEE: WARNING: killing 8766 states (over memory cap)
KLEE: WARNING: killing 9208 states (over memory cap)
KLEE: WARNING: killing 8661 states (over memory cap)
KLEE: WARNING: killing 9009 states (over memory cap)
KLEE: WARNING: killing 9136 states (over memory cap)
KLEE: WARNING: killing 8814 states (over memory cap)
KLEE: WARNING: killing 9253 states (over memory cap)
KLEE: WARNING: killing 8756 states (over memory cap)
KLEE: WARNING: killing 9282 states (over memory cap)
KLEE: WARNING: killing 8966 states (over memory cap)
KLEE: WARNING: killing 8733 states (over memory cap)
KLEE: WARNING: killing 8905 states (over memory cap)
KLEE: WARNING: killing 9209 states (over memory cap)
KLEE: WARNING: killing 8979 states (over memory cap)
KLEE: WARNING: killing 9017 states (over memory cap)
KLEE: WARNING: killing 9142 states (over memory cap)
KLEE: WARNING: killing 8867 states (over memory cap)
KLEE: WARNING: killing 8592 states (over memory cap)
KLEE: WARNING: killing 8850 states (over memory cap)
KLEE: WARNING: killing 9061 states (over memory cap)
KLEE: WARNING: killing 8879 states (over memory cap)
KLEE: WARNING: killing 9002 states (over memory cap)
KLEE: WARNING: killing 8995 states (over memory cap)
KLEE: WARNING: killing 9034 states (over memory cap)
KLEE: WARNING: killing 8765 states (over memory cap)
KLEE: WARNING: killing 8887 states (over memory cap)
KLEE: WARNING: killing 8616 states (over memory cap)
KLEE: WARNING: killing 9181 states (over memory cap)
KLEE: WARNING: killing 9214 states (over memory cap)
KLEE: WARNING: killing 8944 states (over memory cap)
KLEE: WARNING: killing 9200 states (over memory cap)
KLEE: WARNING: killing 8886 states (over memory cap)
KLEE: WARNING: killing 9449 states (over memory cap)
KLEE: WARNING: killing 8919 states (over memory cap)
KLEE: WARNING: killing 9526 states (over memory cap)
KLEE: WARNING: killing 8998 states (over memory cap)
KLEE: WARNING: killing 8946 states (over memory cap)
KLEE: WARNING: killing 9242 states (over memory cap)
KLEE: WARNING: killing 8628 states (over memory cap)
KLEE: WARNING: killing 8837 states (over memory cap)
KLEE: WARNING: killing 8956 states (over memory cap)
KLEE: WARNING: killing 8779 states (over memory cap)
KLEE: WARNING: killing 9030 states (over memory cap)
KLEE: WARNING: killing 8544 states (over memory cap)
KLEE: WARNING: killing 8754 states (over memory cap)
KLEE: WARNING: killing 9137 states (over memory cap)
KLEE: WARNING: killing 8913 states (over memory cap)
KLEE: WARNING: killing 8990 states (over memory cap)
KLEE: WARNING: killing 8725 states (over memory cap)
KLEE: WARNING: killing 8848 states (over memory cap)
KLEE: WARNING: killing 8841 states (over memory cap)
KLEE: WARNING: killing 8706 states (over memory cap)
KLEE: WARNING: killing 9045 states (over memory cap)
KLEE: WARNING: killing 8781 states (over memory cap)
KLEE: WARNING: killing 8944 states (over memory cap)
KLEE: WARNING: killing 9153 states (over memory cap)
KLEE: WARNING: killing 8932 states (over memory cap)
KLEE: WARNING: killing 8799 states (over memory cap)
KLEE: WARNING: killing 8834 states (over memory cap)
KLEE: WARNING: killing 8829 states (over memory cap)
KLEE: WARNING: killing 8732 states (over memory cap)
KLEE: WARNING: killing 9502 states (over memory cap)
KLEE: WARNING: killing 9194 states (over memory cap)
KLEE: WARNING: killing 8888 states (over memory cap)
KLEE: WARNING: killing 8711 states (over memory cap)
KLEE: WARNING: killing 8957 states (over memory cap)
KLEE: WARNING: killing 8866 states (over memory cap)
KLEE: WARNING: killing 8859 states (over memory cap)
KLEE: WARNING: killing 9068 states (over memory cap)
KLEE: WARNING: killing 8894 states (over memory cap)
KLEE: WARNING: killing 8933 states (over memory cap)
KLEE: WARNING: killing 9353 states (over memory cap)
KLEE: WARNING: killing 8749 states (over memory cap)
KLEE: WARNING: killing 8742 states (over memory cap)
KLEE: WARNING: killing 8902 states (over memory cap)
KLEE: WARNING: killing 9535 states (over memory cap)
KLEE: WARNING: killing 9067 states (over memory cap)
KLEE: WARNING: killing 9101 states (over memory cap)
KLEE: WARNING: killing 8966 states (over memory cap)
KLEE: WARNING: killing 8710 states (over memory cap)
KLEE: WARNING: killing 8573 states (over memory cap)
KLEE: WARNING: killing 8735 states (over memory cap)
KLEE: WARNING: killing 8982 states (over memory cap)
KLEE: WARNING: killing 9102 states (over memory cap)
KLEE: WARNING: killing 8589 states (over memory cap)
