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--net--fddi--skfp--skfp.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.: 234 354 4894 36475
Removed infinite loop in dma_unmap_single_attrs
Removed infinite loop in dma_map_single_attrs
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 1.16141295433
Removed calls to 'pci_set_master' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'dma_free_attrs' (function is undefined)
Removed calls to 'free_netdev' (function is undefined)
Removed calls to 'iounmap' (function is undefined)
Removed calls to 'pci_release_regions' (function is undefined)
Removed calls to 'pci_disable_device' (function is undefined)
Removed calls to 'unregister_netdev' (function is undefined)
Defining function printk as symbolic
Defining function pci_enable_device as symbolic
Defining function pci_request_regions as symbolic
Defining function alloc_fddidev as symbolic
Defining function register_netdev as symbolic
Removed calls to 'iowrite16' (function is undefined)
Removed calls to 'iowrite8' (function is undefined)
Defining function ioread8 as symbolic
Removed calls to 'iowrite32' (function is undefined)
Defining function ioread32 as symbolic
Defining function dma_alloc_attrs as symbolic
Defining function ioremap_nocache as symbolic
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'skb_queue_purge' (function is undefined)
Removed calls to 'consume_skb' (function is undefined)
Removed calls to 'skb_queue_tail' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to '__might_fault' (function is undefined)
Removed calls to '__copy_to_user_overflow' (function is undefined)
Defining function fddi_change_mtu as symbolic
Defining function capable as symbolic
Defining function _copy_to_user as symbolic
Defining function _copy_from_user as symbolic
Defining function _raw_spin_lock_irqsave as symbolic
Defining function ioread16 as symbolic
Removed calls to '__dev_kfree_skb_irq' (function is undefined)
Removed calls to 'debug_dma_unmap_page' (function is undefined)
Removed calls to 'skb_trim' (function is undefined)
Defining function skb_put as symbolic
Removed calls to 'debug_dma_map_page' (function is undefined)
Defining function __phys_addr as symbolic
Defining function __alloc_skb as symbolic
Defining function skb_pull as symbolic
Defining function fddi_type_trans as symbolic
Defining function netif_rx as symbolic
Removed calls to 'skb_queue_head' (function is undefined)
Defining function skb_dequeue as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function request_threaded_irq as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'pci_unregister_driver' (function is undefined)
Defining function ldv_ndo_init_3 as symbolic
Defining function ldv_ndo_uninit_3 as symbolic
Defining function ldv_shutdown_2 as symbolic
Defining function __pci_register_driver as symbolic
Linked our definitions to these undefined functions:
  memcmp
  strcpy
  __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: 1.11989784241
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 373 246 2571 17963
INFO: Starting verification
KLEE: WARNING ONCE: function "skfp_open" has inline asm
KLEE: WARNING ONCE: function "skfp_close" has inline asm
KLEE: WARNING ONCE: function "skfp_send_pkt" has inline asm
KLEE: WARNING ONCE: function "pci_unmap_single" has inline asm
KLEE: WARNING ONCE: function "pci_map_single" has inline asm
KLEE: WARNING ONCE: function "llc_restart_tx" 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_3a7ef393-7826-45b0-a628-2baff1609493/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 8945 states (over memory cap)
KLEE: WARNING: killing 9386 states (over memory cap)
KLEE: WARNING: killing 9424 states (over memory cap)
KLEE: WARNING: killing 9661 states (over memory cap)
KLEE: WARNING: killing 9762 states (over memory cap)
KLEE: WARNING: killing 10333 states (over memory cap)
KLEE: WARNING: killing 10440 states (over memory cap)
KLEE: WARNING: killing 10348 states (over memory cap)
KLEE: WARNING: killing 10651 states (over memory cap)
KLEE: WARNING: killing 11094 states (over memory cap)
KLEE: WARNING: killing 10805 states (over memory cap)
KLEE: WARNING: killing 10778 states (over memory cap)
KLEE: WARNING: killing 10757 states (over memory cap)
KLEE: WARNING: killing 10797 states (over memory cap)
KLEE: WARNING: killing 10768 states (over memory cap)
KLEE: WARNING: killing 11075 states (over memory cap)
KLEE: WARNING: killing 10920 states (over memory cap)
KLEE: WARNING: killing 11219 states (over memory cap)
KLEE: WARNING: killing 10996 states (over memory cap)
KLEE: WARNING: killing 10968 states (over memory cap)
KLEE: WARNING: killing 11073 states (over memory cap)
KLEE: WARNING: killing 11048 states (over memory cap)
KLEE: WARNING: killing 10955 states (over memory cap)
KLEE: WARNING: killing 10923 states (over memory cap)
KLEE: WARNING: killing 10965 states (over memory cap)
KLEE: WARNING: killing 11449 states (over memory cap)
KLEE: WARNING: killing 11176 states (over memory cap)
KLEE: WARNING: killing 11082 states (over memory cap)
KLEE: WARNING: killing 10931 states (over memory cap)
KLEE: WARNING: killing 11099 states (over memory cap)
KLEE: WARNING: killing 11012 states (over memory cap)
KLEE: WARNING: killing 11176 states (over memory cap)
KLEE: WARNING: killing 10907 states (over memory cap)
KLEE: WARNING: killing 11131 states (over memory cap)
KLEE: WARNING: killing 11426 states (over memory cap)
KLEE: WARNING: killing 11281 states (over memory cap)
KLEE: WARNING: killing 10948 states (over memory cap)
KLEE: WARNING: killing 10859 states (over memory cap)
KLEE: WARNING: killing 11272 states (over memory cap)
KLEE: WARNING: killing 11190 states (over memory cap)
KLEE: WARNING: killing 11539 states (over memory cap)
KLEE: WARNING: killing 11148 states (over memory cap)
KLEE: WARNING: killing 11005 states (over memory cap)
KLEE: WARNING: killing 11041 states (over memory cap)
KLEE: WARNING: killing 11023 states (over memory cap)
KLEE: WARNING: killing 11490 states (over memory cap)
KLEE: WARNING: killing 11170 states (over memory cap)
KLEE: WARNING: killing 11025 states (over memory cap)
KLEE: WARNING: killing 6151 states (over memory cap)
KLEE: WARNING: killing 10811 states (over memory cap)
KLEE: WARNING: killing 11039 states (over memory cap)
KLEE: WARNING: killing 11316 states (over memory cap)
KLEE: WARNING: killing 10742 states (over memory cap)
KLEE: WARNING: killing 11330 states (over memory cap)
KLEE: WARNING: killing 6030 states (over memory cap)
KLEE: WARNING: killing 10702 states (over memory cap)
KLEE: WARNING: killing 6011 states (over memory cap)
KLEE: WARNING: killing 10975 states (over memory cap)
KLEE: WARNING: killing 6119 states (over memory cap)
KLEE: WARNING: killing 11011 states (over memory cap)
KLEE: WARNING: killing 11048 states (over memory cap)
KLEE: WARNING: killing 11028 states (over memory cap)
KLEE: WARNING: killing 11129 states (over memory cap)
KLEE: WARNING: killing 6129 states (over memory cap)
KLEE: WARNING: killing 11045 states (over memory cap)
KLEE: WARNING: killing 10725 states (over memory cap)
KLEE: WARNING: killing 5983 states (over memory cap)
KLEE: WARNING: killing 10996 states (over memory cap)
KLEE: WARNING: killing 5909 states (over memory cap)
KLEE: WARNING: killing 10726 states (over memory cap)
KLEE: WARNING: killing 6068 states (over memory cap)
KLEE: WARNING: killing 10639 states (over memory cap)
KLEE: WARNING: killing 6227 states (over memory cap)
KLEE: WARNING: killing 10611 states (over memory cap)
KLEE: WARNING: killing 5918 states (over memory cap)
KLEE: WARNING: killing 10765 states (over memory cap)
KLEE: WARNING: killing 11096 states (over memory cap)
KLEE: WARNING: killing 6013 states (over memory cap)
KLEE: WARNING: killing 10780 states (over memory cap)
KLEE: WARNING: killing 5942 states (over memory cap)
KLEE: WARNING: killing 10925 states (over memory cap)
KLEE: WARNING: killing 5983 states (over memory cap)
KLEE: WARNING: killing 10667 states (over memory cap)
KLEE: WARNING: killing 6198 states (over memory cap)
KLEE: WARNING: killing 10755 states (over memory cap)
KLEE: WARNING: killing 5954 states (over memory cap)
KLEE: WARNING: killing 10612 states (over memory cap)
klee: /var/xchalup4/symbiotic/klee/include/klee/Internal/ADT/DiscretePDF.inc:116: void klee::DiscretePDF<T>::remove(T) [with T = klee::ExecutionState*]: Assertion `0 && "remove: argument(item) not in tree"' failed.
KLEE: output directory is "/tmp/symbiotic-HwZ3c4/klee-out-0"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: function "skfp_open" has inline asm
KLEE: WARNING ONCE: function "skfp_close" has inline asm
KLEE: WARNING ONCE: function "skfp_send_pkt" has inline asm
KLEE: WARNING ONCE: function "pci_unmap_single" has inline asm
KLEE: WARNING ONCE: function "pci_map_single" has inline asm
KLEE: WARNING ONCE: function "llc_restart_tx" 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_3a7ef393-7826-45b0-a628-2baff1609493/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 8945 states (over memory cap)
KLEE: WARNING: killing 9386 states (over memory cap)
KLEE: WARNING: killing 9424 states (over memory cap)
KLEE: WARNING: killing 9661 states (over memory cap)
KLEE: WARNING: killing 9762 states (over memory cap)
KLEE: WARNING: killing 10333 states (over memory cap)
KLEE: WARNING: killing 10440 states (over memory cap)
KLEE: WARNING: killing 10348 states (over memory cap)
KLEE: WARNING: killing 10651 states (over memory cap)
KLEE: WARNING: killing 11094 states (over memory cap)
KLEE: WARNING: killing 10805 states (over memory cap)
KLEE: WARNING: killing 10778 states (over memory cap)
KLEE: WARNING: killing 10757 states (over memory cap)
KLEE: WARNING: killing 10797 states (over memory cap)
KLEE: WARNING: killing 10768 states (over memory cap)
KLEE: WARNING: killing 11075 states (over memory cap)
KLEE: WARNING: killing 10920 states (over memory cap)
KLEE: WARNING: killing 11219 states (over memory cap)
KLEE: WARNING: killing 10996 states (over memory cap)
KLEE: WARNING: killing 10968 states (over memory cap)
KLEE: WARNING: killing 11073 states (over memory cap)
KLEE: WARNING: killing 11048 states (over memory cap)
KLEE: WARNING: killing 10955 states (over memory cap)
KLEE: WARNING: killing 10923 states (over memory cap)
KLEE: WARNING: killing 10965 states (over memory cap)
KLEE: WARNING: killing 11449 states (over memory cap)
KLEE: WARNING: killing 11176 states (over memory cap)
KLEE: WARNING: killing 11082 states (over memory cap)
KLEE: WARNING: killing 10931 states (over memory cap)
KLEE: WARNING: killing 11099 states (over memory cap)
KLEE: WARNING: killing 11012 states (over memory cap)
KLEE: WARNING: killing 11176 states (over memory cap)
KLEE: WARNING: killing 10907 states (over memory cap)
KLEE: WARNING: killing 11131 states (over memory cap)
KLEE: WARNING: killing 11426 states (over memory cap)
KLEE: WARNING: killing 11281 states (over memory cap)
KLEE: WARNING: killing 10948 states (over memory cap)
KLEE: WARNING: killing 10859 states (over memory cap)
KLEE: WARNING: killing 11272 states (over memory cap)
KLEE: WARNING: killing 11190 states (over memory cap)
KLEE: WARNING: killing 11539 states (over memory cap)
KLEE: WARNING: killing 11148 states (over memory cap)
KLEE: WARNING: killing 11005 states (over memory cap)
KLEE: WARNING: killing 11041 states (over memory cap)
KLEE: WARNING: killing 11023 states (over memory cap)
KLEE: WARNING: killing 11490 states (over memory cap)
KLEE: WARNING: killing 11170 states (over memory cap)
KLEE: WARNING: killing 11025 states (over memory cap)
KLEE: WARNING: killing 6151 states (over memory cap)
KLEE: WARNING: killing 10811 states (over memory cap)
KLEE: WARNING: killing 11039 states (over memory cap)
KLEE: WARNING: killing 11316 states (over memory cap)
KLEE: WARNING: killing 10742 states (over memory cap)
KLEE: WARNING: killing 11330 states (over memory cap)
KLEE: WARNING: killing 6030 states (over memory cap)
KLEE: WARNING: killing 10702 states (over memory cap)
KLEE: WARNING: killing 6011 states (over memory cap)
KLEE: WARNING: killing 10975 states (over memory cap)
KLEE: WARNING: killing 6119 states (over memory cap)
KLEE: WARNING: killing 11011 states (over memory cap)
KLEE: WARNING: killing 11048 states (over memory cap)
KLEE: WARNING: killing 11028 states (over memory cap)
KLEE: WARNING: killing 11129 states (over memory cap)
KLEE: WARNING: killing 6129 states (over memory cap)
KLEE: WARNING: killing 11045 states (over memory cap)
KLEE: WARNING: killing 10725 states (over memory cap)
KLEE: WARNING: killing 5983 states (over memory cap)
KLEE: WARNING: killing 10996 states (over memory cap)
KLEE: WARNING: killing 5909 states (over memory cap)
KLEE: WARNING: killing 10726 states (over memory cap)
KLEE: WARNING: killing 6068 states (over memory cap)
KLEE: WARNING: killing 10639 states (over memory cap)
KLEE: WARNING: killing 6227 states (over memory cap)
KLEE: WARNING: killing 10611 states (over memory cap)
KLEE: WARNING: killing 5918 states (over memory cap)
KLEE: WARNING: killing 10765 states (over memory cap)
KLEE: WARNING: killing 11096 states (over memory cap)
KLEE: WARNING: killing 6013 states (over memory cap)
KLEE: WARNING: killing 10780 states (over memory cap)
KLEE: WARNING: killing 5942 states (over memory cap)
KLEE: WARNING: killing 10925 states (over memory cap)
KLEE: WARNING: killing 5983 states (over memory cap)
KLEE: WARNING: killing 10667 states (over memory cap)
KLEE: WARNING: killing 6198 states (over memory cap)
KLEE: WARNING: killing 10755 states (over memory cap)
KLEE: WARNING: killing 5954 states (over memory cap)
KLEE: WARNING: killing 10612 states (over memory cap)
klee: /var/xchalup4/symbiotic/klee/include/klee/Internal/ADT/DiscretePDF.inc:116: void klee::DiscretePDF<T>::remove(T) [with T = klee::ExecutionState*]: Assertion `0 && "remove: argument(item) not in tree"' failed.
0  klee            0x00000000012fcca8 llvm::sys::PrintStackTrace(llvm::raw_ostream&) + 56
1  klee            0x00000000012fac7e llvm::sys::RunSignalHandlers() + 62
2  klee            0x00000000012fadcc
3  libpthread.so.0 0x00007f71c70ab390
4  libc.so.6       0x00007f71c6464428 gsignal + 56
5  libc.so.6       0x00007f71c646602a abort + 362
6  libc.so.6       0x00007f71c645cbd7
7  libc.so.6       0x00007f71c645cc82
8  klee            0x000000000061be59 klee::DiscretePDF<klee::ExecutionState*>::remove(klee::ExecutionState*) + 73
9  klee            0x00000000006195f1 klee::WeightedRandomSearcher::update(klee::ExecutionState*, std::vector<klee::ExecutionState*, std::allocator<klee::ExecutionState*> > const&, std::vector<klee::ExecutionState*, std::allocator<klee::ExecutionState*> > const&) + 241
10 klee            0x0000000000617416 klee::InterleavedSearcher::update(klee::ExecutionState*, std::vector<klee::ExecutionState*, std::allocator<klee::ExecutionState*> > const&, std::vector<klee::ExecutionState*, std::allocator<klee::ExecutionState*> > const&) + 54
11 klee            0x00000000005cecfe klee::Executor::updateStates(klee::ExecutionState*) + 46
12 klee            0x00000000005da8eb klee::Executor::run(klee::ExecutionState&) + 2155
13 klee            0x00000000005daeef klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1391
14 klee            0x0000000000593c63 main + 8867
15 libc.so.6       0x00007f71c644f830 __libc_start_main + 240
16 klee            0x00000000005bed49 _start + 41
Running the verifier failed
RESULT: unknown
INFO: Total time elapsed: 501.566644907
