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--media--usb--em28xx--em28xx-dvb.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.: 154 82 1296 9543
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 0.456094026566
Removed calls to '__const_udelay' (function is undefined)
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to '__symbol_put' (function is undefined)
Removed calls to 'dvb_frontend_detach' (function is undefined)
Removed calls to 'gpio_free' (function is undefined)
Removed calls to 'msleep' (function is undefined)
Removed calls to 'i2c_unregister_device' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'dvb_dmxdev_release' (function is undefined)
Removed calls to 'dvb_dmx_release' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'em28xx_uninit_usb_xfer' (function is undefined)
Removed calls to 'dvb_net_release' (function is undefined)
Removed calls to 'em28xx_free_device' (function is undefined)
Defining function printk as symbolic
Defining function dvb_frontend_resume as symbolic
Defining function dvb_frontend_suspend as symbolic
Defining function dvb_unregister_frontend as symbolic
Defining function dvb_unregister_adapter as symbolic
Defining function em28xx_alloc_urbs as symbolic
Defining function em28xx_set_mode as symbolic
Defining function __symbol_get as symbolic
Defining function __request_module as symbolic
Removed calls to 'em28xx_setup_xc3028' (function is undefined)
Defining function gpio_request_one as symbolic
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to 'down' (function is undefined)
Removed calls to 'up' (function is undefined)
Defining function strlcpy as symbolic
Defining function i2c_new_device as symbolic
Defining function em28xx_tuner_callback as symbolic
Defining function dvb_register_adapter as symbolic
Defining function dvb_register_frontend as symbolic
Removed calls to 'em28xx_stop_urbs' (function is undefined)
Defining function dvb_dmx_init as symbolic
Defining function dvb_dmxdev_init as symbolic
Defining function dvb_net_init as symbolic
Defining function usb_set_interface as symbolic
Removed calls to 'dvb_dmx_swfilter' (function is undefined)
Defining function em28xx_init_usb_xfer as symbolic
Defining function em28xx_write_reg_bits as symbolic
Defining function em28xx_write_reg as symbolic
Defining function em28xx_gpio_set as symbolic
Defining function i2c_master_send as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'em28xx_unregister_extension' (function is undefined)
Defining function ldv_stop_1 as symbolic
Defining function ldv_disconnect_1 as symbolic
Defining function ldv_release_1 as symbolic
Defining function ldv_bind_1 as symbolic
Defining function ldv_start_1 as symbolic
Defining function em28xx_register_extension as symbolic
Linked our definitions to these undefined functions:
  __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.436748027802
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 243 100 866 6049
INFO: Starting verification
KLEE: WARNING ONCE: function "em28xx_dvb_init" has inline asm
KLEE: WARNING ONCE: function "em28xx_dvb_fini" 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_87213253-41f9-42b0-96c7-a93078a36361/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 10603 states (over memory cap)
KLEE: WARNING: killing 12210 states (over memory cap)
KLEE: WARNING: killing 12150 states (over memory cap)
KLEE: WARNING: killing 12180 states (over memory cap)
KLEE: WARNING: killing 12300 states (over memory cap)
KLEE: WARNING: killing 8740 states (over memory cap)
KLEE: WARNING: killing 8811 states (over memory cap)
KLEE: WARNING: killing 8791 states (over memory cap)
KLEE: WARNING: killing 8944 states (over memory cap)
KLEE: WARNING: killing 8928 states (over memory cap)
KLEE: WARNING: killing 8996 states (over memory cap)
KLEE: WARNING: killing 9151 states (over memory cap)
KLEE: WARNING: killing 9218 states (over memory cap)
KLEE: WARNING: killing 9032 states (over memory cap)
KLEE: WARNING: killing 9351 states (over memory cap)
KLEE: WARNING: killing 9165 states (over memory cap)
KLEE: WARNING: killing 9322 states (over memory cap)
KLEE: WARNING: killing 9137 states (over memory cap)
KLEE: WARNING: killing 9627 states (over memory cap)
KLEE: WARNING: killing 10037 states (over memory cap)
KLEE: WARNING: killing 9689 states (over memory cap)
KLEE: WARNING: killing 10262 states (over memory cap)
KLEE: WARNING: killing 9911 states (over memory cap)
KLEE: WARNING: killing 9979 states (over memory cap)
KLEE: WARNING: killing 9793 states (over memory cap)
KLEE: WARNING: killing 10370 states (over memory cap)
KLEE: WARNING: killing 10026 states (over memory cap)
KLEE: WARNING: killing 9918 states (over memory cap)
KLEE: WARNING: killing 9817 states (over memory cap)
KLEE: WARNING: killing 10296 states (over memory cap)
KLEE: WARNING: killing 10108 states (over memory cap)
KLEE: WARNING: killing 10248 states (over memory cap)
KLEE: WARNING: killing 10235 states (over memory cap)
KLEE: WARNING: killing 10462 states (over memory cap)
KLEE: WARNING: killing 10198 states (over memory cap)
KLEE: WARNING: killing 10184 states (over memory cap)
KLEE: WARNING: killing 10488 states (over memory cap)
KLEE: WARNING: killing 10385 states (over memory cap)
KLEE: WARNING: killing 10362 states (over memory cap)
KLEE: WARNING: killing 10668 states (over memory cap)
KLEE: WARNING: killing 10725 states (over memory cap)
KLEE: WARNING: killing 10791 states (over memory cap)
KLEE: WARNING: killing 10442 states (over memory cap)
KLEE: WARNING: killing 10343 states (over memory cap)
KLEE: WARNING: killing 10883 states (over memory cap)
KLEE: WARNING: killing 10380 states (over memory cap)
KLEE: WARNING: killing 10684 states (over memory cap)
KLEE: WARNING: killing 10666 states (over memory cap)
KLEE: WARNING: killing 10484 states (over memory cap)
KLEE: WARNING: killing 10545 states (over memory cap)
KLEE: WARNING: killing 10047 states (over memory cap)
KLEE: WARNING: killing 10576 states (over memory cap)
KLEE: WARNING: killing 10078 states (over memory cap)
KLEE: WARNING: killing 10845 states (over memory cap)
KLEE: WARNING: killing 10743 states (over memory cap)
KLEE: WARNING: killing 10332 states (over memory cap)
KLEE: WARNING: killing 11028 states (over memory cap)
KLEE: WARNING: killing 10609 states (over memory cap)
KLEE: WARNING: killing 10503 states (over memory cap)
KLEE: WARNING: killing 10798 states (over memory cap)
KLEE: WARNING: killing 10308 states (over memory cap)
KLEE: WARNING: killing 10370 states (over memory cap)
KLEE: WARNING: killing 10664 states (over memory cap)
KLEE: WARNING: killing 10567 states (over memory cap)
KLEE: WARNING: killing 10704 states (over memory cap)
KLEE: WARNING: killing 10690 states (over memory cap)
KLEE: WARNING: killing 10748 states (over memory cap)
KLEE: WARNING: killing 10800 states (over memory cap)
KLEE: WARNING: killing 10396 states (over memory cap)
KLEE: WARNING: killing 10685 states (over memory cap)
KLEE: WARNING: killing 10665 states (over memory cap)
KLEE: WARNING: killing 10640 states (over memory cap)
KLEE: WARNING: killing 10624 states (over memory cap)
KLEE: WARNING: killing 10756 states (over memory cap)
KLEE: WARNING: killing 10661 states (over memory cap)
KLEE: WARNING: killing 10420 states (over memory cap)
KLEE: WARNING: killing 10786 states (over memory cap)
KLEE: WARNING: killing 10693 states (over memory cap)
KLEE: WARNING: killing 10981 states (over memory cap)
KLEE: WARNING: killing 10733 states (over memory cap)
KLEE: WARNING: killing 10260 states (over memory cap)
KLEE: WARNING: killing 10621 states (over memory cap)
KLEE: WARNING: killing 10825 states (over memory cap)
KLEE: WARNING: killing 10955 states (over memory cap)
KLEE: WARNING: killing 10487 states (over memory cap)
KLEE: WARNING: killing 10396 states (over memory cap)
KLEE: WARNING: killing 10597 states (over memory cap)
KLEE: WARNING: killing 10729 states (over memory cap)
KLEE: WARNING: killing 10412 states (over memory cap)
KLEE: WARNING: killing 10618 states (over memory cap)
KLEE: WARNING: killing 10752 states (over memory cap)
KLEE: WARNING: killing 10958 states (over memory cap)
KLEE: WARNING: killing 10568 states (over memory cap)
KLEE: WARNING: killing 10336 states (over memory cap)
KLEE: WARNING: killing 10757 states (over memory cap)
KLEE: WARNING: killing 10738 states (over memory cap)
KLEE: WARNING: killing 10721 states (over memory cap)
KLEE: WARNING: killing 10550 states (over memory cap)
KLEE: WARNING: killing 10900 states (over memory cap)
KLEE: WARNING: killing 10664 states (over memory cap)
KLEE: WARNING: killing 10640 states (over memory cap)
KLEE: WARNING: killing 10769 states (over memory cap)
KLEE: WARNING: killing 10533 states (over memory cap)
KLEE: WARNING: killing 10519 states (over memory cap)
KLEE: WARNING: killing 10720 states (over memory cap)
KLEE: WARNING: killing 10337 states (over memory cap)
KLEE: WARNING: killing 10751 states (over memory cap)
KLEE: WARNING: killing 10804 states (over memory cap)
KLEE: WARNING: killing 10648 states (over memory cap)
KLEE: WARNING: killing 10562 states (over memory cap)
KLEE: WARNING: killing 10476 states (over memory cap)
KLEE: WARNING: killing 10602 states (over memory cap)
KLEE: WARNING: killing 10804 states (over memory cap)
KLEE: WARNING: killing 10354 states (over memory cap)
