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--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.: 236 502 5151 38098
Removed infinite loop in dma_unmap_single_attrs
Removed infinite loop in dma_map_single_attrs
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 1.13768100739
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
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function mutex_trylock 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.14234900475
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 375 395 3012 19220
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_efd8999e-2a6b-4f79-a02c-2a61d6d652c0/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 7955 states (over memory cap)
KLEE: WARNING: killing 9678 states (over memory cap)
KLEE: WARNING: killing 9778 states (over memory cap)
KLEE: WARNING: killing 9948 states (over memory cap)
KLEE: WARNING: killing 10055 states (over memory cap)
KLEE: WARNING: killing 10230 states (over memory cap)
KLEE: WARNING: killing 10133 states (over memory cap)
KLEE: WARNING: killing 10370 states (over memory cap)
KLEE: WARNING: killing 10878 states (over memory cap)
KLEE: WARNING: killing 11053 states (over memory cap)
KLEE: WARNING: killing 10759 states (over memory cap)
KLEE: WARNING: killing 10603 states (over memory cap)
KLEE: WARNING: killing 10778 states (over memory cap)
KLEE: WARNING: killing 10557 states (over memory cap)
KLEE: WARNING: killing 10990 states (over memory cap)
KLEE: WARNING: killing 10901 states (over memory cap)
KLEE: WARNING: killing 11133 states (over memory cap)
KLEE: WARNING: killing 10649 states (over memory cap)
KLEE: WARNING: killing 10493 states (over memory cap)
KLEE: WARNING: killing 11181 states (over memory cap)
KLEE: WARNING: killing 11281 states (over memory cap)
KLEE: WARNING: killing 11001 states (over memory cap)
KLEE: WARNING: killing 10976 states (over memory cap)
KLEE: WARNING: killing 11467 states (over memory cap)
KLEE: WARNING: killing 11119 states (over memory cap)
KLEE: WARNING: killing 11094 states (over memory cap)
KLEE: WARNING: killing 11070 states (over memory cap)
KLEE: WARNING: killing 10921 states (over memory cap)
KLEE: WARNING: killing 10954 states (over memory cap)
KLEE: WARNING: killing 11317 states (over memory cap)
KLEE: WARNING: killing 10915 states (over memory cap)
KLEE: WARNING: killing 11334 states (over memory cap)
KLEE: WARNING: killing 11053 states (over memory cap)
KLEE: WARNING: killing 11223 states (over memory cap)
KLEE: WARNING: killing 11012 states (over memory cap)
KLEE: WARNING: killing 11298 states (over memory cap)
KLEE: WARNING: killing 11219 states (over memory cap)
KLEE: WARNING: killing 11443 states (over memory cap)
KLEE: WARNING: killing 11300 states (over memory cap)
KLEE: WARNING: killing 11278 states (over memory cap)
KLEE: WARNING: killing 11128 states (over memory cap)
KLEE: WARNING: killing 11046 states (over memory cap)
KLEE: WARNING: killing 11085 states (over memory cap)
KLEE: WARNING: killing 11246 states (over memory cap)
KLEE: WARNING: killing 11105 states (over memory cap)
KLEE: WARNING: killing 6200 states (over memory cap)
KLEE: WARNING: killing 10893 states (over memory cap)
KLEE: WARNING: killing 11363 states (over memory cap)
KLEE: WARNING: killing 10969 states (over memory cap)
KLEE: WARNING: killing 11008 states (over memory cap)
KLEE: WARNING: killing 6265 states (over memory cap)
KLEE: WARNING: killing 10550 states (over memory cap)
KLEE: WARNING: killing 6127 states (over memory cap)
KLEE: WARNING: killing 10888 states (over memory cap)
KLEE: WARNING: killing 11233 states (over memory cap)
KLEE: WARNING: killing 6342 states (over memory cap)
KLEE: WARNING: killing 10964 states (over memory cap)
KLEE: WARNING: killing 10943 states (over memory cap)
KLEE: WARNING: killing 10803 states (over memory cap)
KLEE: WARNING: killing 11080 states (over memory cap)
KLEE: WARNING: killing 6106 states (over memory cap)
KLEE: WARNING: killing 10326 states (over memory cap)
KLEE: WARNING: killing 6029 states (over memory cap)
KLEE: WARNING: killing 10954 states (over memory cap)
KLEE: WARNING: killing 6131 states (over memory cap)
KLEE: WARNING: killing 11230 states (over memory cap)
KLEE: WARNING: killing 6000 states (over memory cap)
KLEE: WARNING: killing 10668 states (over memory cap)
KLEE: WARNING: killing 6046 states (over memory cap)
KLEE: WARNING: killing 10939 states (over memory cap)
KLEE: WARNING: killing 6208 states (over memory cap)
KLEE: WARNING: killing 10918 states (over memory cap)
KLEE: WARNING: killing 11073 states (over memory cap)
KLEE: WARNING: killing 11174 states (over memory cap)
KLEE: WARNING: killing 10618 states (over memory cap)
KLEE: WARNING: killing 6040 states (over memory cap)
KLEE: WARNING: killing 10764 states (over memory cap)
KLEE: WARNING: killing 6023 states (over memory cap)
KLEE: WARNING: killing 10853 states (over memory cap)
KLEE: WARNING: killing 6067 states (over memory cap)
KLEE: WARNING: killing 10536 states (over memory cap)
KLEE: WARNING: killing 6050 states (over memory cap)
KLEE: WARNING: killing 5815 states (over memory cap)
KLEE: WARNING: killing 10851 states (over memory cap)
KLEE: WARNING: killing 6090 states (over memory cap)
KLEE: WARNING: killing 11007 states (over memory cap)
KLEE: WARNING: killing 5961 states (over memory cap)
KLEE: WARNING: killing 10688 states (over memory cap)
KLEE: WARNING: killing 5886 states (over memory cap)
KLEE: WARNING: killing 11007 states (over memory cap)
KLEE: WARNING: killing 5873 states (over memory cap)
KLEE: WARNING: killing 5810 states (over memory cap)
KLEE: WARNING: killing 10681 states (over memory cap)
KLEE: WARNING: killing 5909 states (over memory cap)
KLEE: WARNING: killing 10541 states (over memory cap)
KLEE: WARNING: killing 6011 states (over memory cap)
KLEE: WARNING: killing 10748 states (over memory cap)
KLEE: WARNING: killing 6050 states (over memory cap)
KLEE: WARNING: killing 5704 states (over memory cap)
KLEE: WARNING: killing 10478 states (over memory cap)
KLEE: WARNING: killing 5688 states (over memory cap)
KLEE: WARNING: killing 10906 states (over memory cap)
KLEE: WARNING: killing 6243 states (over memory cap)
KLEE: WARNING: killing 5841 states (over memory cap)
KLEE: WARNING: killing 10709 states (over memory cap)
KLEE: WARNING: killing 6281 states (over memory cap)
KLEE: WARNING: killing 10568 states (over memory cap)
KLEE: WARNING: killing 6097 states (over memory cap)
KLEE: WARNING: killing 10370 states (over memory cap)
KLEE: WARNING: killing 6078 states (over memory cap)
KLEE: WARNING: killing 10740 states (over memory cap)
KLEE: WARNING: killing 5897 states (over memory cap)
KLEE: WARNING: killing 10433 states (over memory cap)
KLEE: WARNING: killing 6329 states (over memory cap)
KLEE: WARNING: killing 5713 states (over memory cap)
KLEE: WARNING: killing 5599 states (over memory cap)
KLEE: WARNING: killing 10678 states (over memory cap)
KLEE: WARNING: killing 6143 states (over memory cap)
KLEE: WARNING: killing 5858 states (over memory cap)
KLEE: WARNING: killing 5578 states (over memory cap)
KLEE: WARNING: killing 10470 states (over memory cap)
KLEE: WARNING: killing 6120 states (over memory cap)
KLEE: WARNING: killing 10505 states (over memory cap)
KLEE: WARNING: killing 6163 states (over memory cap)
KLEE: WARNING: killing 5715 states (over memory cap)
KLEE: WARNING: killing 5600 states (over memory cap)
KLEE: WARNING: killing 5597 states (over memory cap)
KLEE: WARNING: killing 5705 states (over memory cap)
KLEE: WARNING: killing 10510 states (over memory cap)
KLEE: WARNING: killing 6021 states (over memory cap)
KLEE: WARNING: killing 5629 states (over memory cap)
KLEE: WARNING: killing 10587 states (over memory cap)
KLEE: WARNING: killing 6056 states (over memory cap)
KLEE: WARNING: killing 5613 states (over memory cap)
KLEE: WARNING: killing 5612 states (over memory cap)
KLEE: WARNING: killing 5607 states (over memory cap)
KLEE: WARNING: killing 5602 states (over memory cap)
KLEE: WARNING: killing 5545 states (over memory cap)
KLEE: WARNING: killing 10531 states (over memory cap)
KLEE: WARNING: killing 6188 states (over memory cap)
KLEE: WARNING: killing 5583 states (over memory cap)
KLEE: WARNING: killing 5581 states (over memory cap)
KLEE: WARNING: killing 5575 states (over memory cap)
KLEE: WARNING: killing 5681 states (over memory cap)
KLEE: WARNING: killing 10533 states (over memory cap)
KLEE: WARNING: killing 6267 states (over memory cap)
KLEE: WARNING: killing 5503 states (over memory cap)
KLEE: WARNING: killing 5714 states (over memory cap)
KLEE: WARNING: killing 5440 states (over memory cap)
KLEE: WARNING: killing 5598 states (over memory cap)
KLEE: WARNING: killing 5756 states (over memory cap)
KLEE: WARNING: killing 5429 states (over memory cap)
KLEE: WARNING: killing 5425 states (over memory cap)
KLEE: WARNING: killing 5529 states (over memory cap)
KLEE: WARNING: killing 5632 states (over memory cap)
KLEE: WARNING: killing 5629 states (over memory cap)
KLEE: WARNING: killing 5678 states (over memory cap)
KLEE: WARNING: killing 5674 states (over memory cap)
KLEE: WARNING: killing 5511 states (over memory cap)
KLEE: WARNING: killing 5508 states (over memory cap)
KLEE: WARNING: killing 10410 states (over memory cap)
KLEE: WARNING: killing 5922 states (over memory cap)
KLEE: WARNING: killing 5544 states (over memory cap)
KLEE: WARNING: killing 5484 states (over memory cap)
KLEE: WARNING: killing 5643 states (over memory cap)
KLEE: WARNING: killing 5639 states (over memory cap)
KLEE: WARNING: killing 5579 states (over memory cap)
KLEE: WARNING: killing 10348 states (over memory cap)
KLEE: WARNING: killing 6102 states (over memory cap)
KLEE: WARNING: killing 5671 states (over memory cap)
KLEE: WARNING: killing 5722 states (over memory cap)
KLEE: WARNING: killing 5664 states (over memory cap)
KLEE: WARNING: killing 5555 states (over memory cap)
KLEE: WARNING: killing 5659 states (over memory cap)
KLEE: WARNING: killing 5870 states (over memory cap)
KLEE: WARNING: killing 5597 states (over memory cap)
KLEE: WARNING: killing 5378 states (over memory cap)
KLEE: WARNING: killing 5533 states (over memory cap)
KLEE: WARNING: killing 5693 states (over memory cap)
KLEE: WARNING: killing 5426 states (over memory cap)
KLEE: WARNING: killing 5740 states (over memory cap)
KLEE: WARNING: killing 5522 states (over memory cap)
KLEE: WARNING: killing 5464 states (over memory cap)
