bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-challenges/linux-3.8-rc1-32_7a-drivers--net--fddi--skfp--skfp.ko-ldv_main0_sequence_infinite_withcheck_stateful_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.: 218 425 4954 37473
Removed infinite loop in dma_unmap_single_attrs
Removed infinite loop in dma_map_single_attrs
Removed infinite loop in arch_local_save_flags
INFO: Compilation, preparation and instrumentation time: 1.08936095238
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to 'skb_queue_head' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'dev_kfree_skb_irq' (function is undefined)
Defining function skb_dequeue as symbolic
Defining function _raw_spin_lock_irqsave as symbolic
Removed calls to 'debug_dma_map_page' (function is undefined)
Removed calls to 'iowrite32' (function is undefined)
Removed calls to 'debug_dma_unmap_page' (function is undefined)
Removed calls to 'iowrite16' (function is undefined)
Defining function printk as symbolic
Removed calls to 'iowrite8' (function is undefined)
Defining function ioread32 as symbolic
Defining function ioread16 as symbolic
Defining function __phys_addr as symbolic
Removed calls to 'pci_set_master' (function is undefined)
Removed calls to '__raw_spin_lock_init' (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)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'debug_dma_free_coherent' (function is undefined)
Defining function dev_set_drvdata as symbolic
Defining function dev_get_drvdata 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 'debug_dma_alloc_coherent' (function is undefined)
Defining function ioread8 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 'might_fault' (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
Removed calls to 'skb_trim' (function is undefined)
Defining function skb_put 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
Defining function request_threaded_irq as symbolic
Removed calls to 'ldv_handler_precall' (function is undefined)
Removed calls to 'ldv_check_return_value' (function is undefined)
Removed calls to 'ldv_check_return_value_probe' (function is undefined)
Removed calls to 'pci_unregister_driver' (function is undefined)
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
  __memcpy
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 1.05464792252
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 360 314 2756 18426
INFO: Starting verification
KLEE: WARNING ONCE: function "llc_restart_tx" has inline asm
KLEE: WARNING ONCE: function "pci_map_single" has inline asm
KLEE: WARNING ONCE: function "pci_unmap_single" has inline asm
KLEE: WARNING ONCE: function "pci_free_consistent" has inline asm
KLEE: WARNING ONCE: function "skfp_open" has inline asm
KLEE: WARNING ONCE: function "skfp_send_pkt" has inline asm
KLEE: WARNING ONCE: function "netif_stop_queue" has inline asm
KLEE: ERROR: /tmp/symbiotic-G2yESm/linux-3.8-rc1-32_7a-drivers--net--fddi--skfp--skfp.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:6879: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-G2yESm/linux-3.8-rc1-32_7a-drivers--net--fddi--skfp--skfp.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:6879: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-G2yESm/linux-3.8-rc1-32_7a-drivers--net--fddi--skfp--skfp.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:6880: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-G2yESm/linux-3.8-rc1-32_7a-drivers--net--fddi--skfp--skfp.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:6845: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-G2yESm/linux-3.8-rc1-32_7a-drivers--net--fddi--skfp--skfp.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:7082: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-G2yESm/linux-3.8-rc1-32_7a-drivers--net--fddi--skfp--skfp.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:6784: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-G2yESm/linux-3.8-rc1-32_7a-drivers--net--fddi--skfp--skfp.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:20179: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-G2yESm/linux-3.8-rc1-32_7a-drivers--net--fddi--skfp--skfp.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:6493: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-G2yESm/linux-3.8-rc1-32_7a-drivers--net--fddi--skfp--skfp.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:7051: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-G2yESm/linux-3.8-rc1-32_7a-drivers--net--fddi--skfp--skfp.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:6500: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-G2yESm/linux-3.8-rc1-32_7a-drivers--net--fddi--skfp--skfp.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:6926: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-G2yESm/linux-3.8-rc1-32_7a-drivers--net--fddi--skfp--skfp.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:6879: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-G2yESm/linux-3.8-rc1-32_7a-drivers--net--fddi--skfp--skfp.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:6879: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-G2yESm/linux-3.8-rc1-32_7a-drivers--net--fddi--skfp--skfp.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:11308: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-G2yESm/linux-3.8-rc1-32_7a-drivers--net--fddi--skfp--skfp.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:11311: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-G2yESm/linux-3.8-rc1-32_7a-drivers--net--fddi--skfp--skfp.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:6880: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-G2yESm/linux-3.8-rc1-32_7a-drivers--net--fddi--skfp--skfp.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:7142: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-G2yESm/linux-3.8-rc1-32_7a-drivers--net--fddi--skfp--skfp.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:7143: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-G2yESm/linux-3.8-rc1-32_7a-drivers--net--fddi--skfp--skfp.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:7143: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-G2yESm/linux-3.8-rc1-32_7a-drivers--net--fddi--skfp--skfp.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:11331: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-G2yESm/linux-3.8-rc1-32_7a-drivers--net--fddi--skfp--skfp.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:7150: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-G2yESm/linux-3.8-rc1-32_7a-drivers--net--fddi--skfp--skfp.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:11232: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-G2yESm/linux-3.8-rc1-32_7a-drivers--net--fddi--skfp--skfp.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:6516: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-G2yESm/linux-3.8-rc1-32_7a-drivers--net--fddi--skfp--skfp.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:6516: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-G2yESm/linux-3.8-rc1-32_7a-drivers--net--fddi--skfp--skfp.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:6516: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-G2yESm/linux-3.8-rc1-32_7a-drivers--net--fddi--skfp--skfp.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:20193: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-G2yESm/linux-3.8-rc1-32_7a-drivers--net--fddi--skfp--skfp.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:20180: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-G2yESm/linux-3.8-rc1-32_7a-drivers--net--fddi--skfp--skfp.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:6517: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-G2yESm/linux-3.8-rc1-32_7a-drivers--net--fddi--skfp--skfp.ko-ldv_main0_sequence_infinite_withcheck_stateful_true-unreach-call.cil.out.c:7143: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
