bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.14/linux-3.14__linux-kernel-locking-mutex__drivers-net-fddi-skfp-skfp_true-unreach-call.cil.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.: 220 429 6166 40679
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 1.18455910683
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)
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)
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
Defining function ldv_pre_register_netdev as symbolic
Defining function fddi_change_mtu as symbolic
Removed calls to 'might_fault' (function is undefined)
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 ioread8 as symbolic
Removed calls to 'skb_queue_tail' (function is undefined)
Removed calls to 'ldv_switch_to_interrupt_context' (function is undefined)
Removed calls to 'ldv_switch_to_process_context' (function is undefined)
Defining function request_threaded_irq as symbolic
Removed calls to 'debug_dma_alloc_coherent' (function is undefined)
Defining function ioremap_nocache as symbolic
Removed calls to 'pci_unregister_driver' (function is undefined)
Defining function __pci_register_driver as symbolic
Removed calls to 'ldv_pre_probe' (function is undefined)
Removed calls to 'ldv_check_alloc_flags' (function is undefined)
Removed calls to 'ldv_after_alloc' (function is undefined)
Removed calls to 'ldv_assert' (function is undefined)
Defining function external_allocated_data 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.12142300606
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 324 309 2674 17180
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 "netif_stop_queue" 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: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_81000367-8666-4b18-9187-049e49ba1418/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-65LBpG/linux-3.14__linux-kernel-locking-mutex__drivers-net-fddi-skfp-skfp_true-unreach-call.cil.c:7200: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-65LBpG/linux-3.14__linux-kernel-locking-mutex__drivers-net-fddi-skfp-skfp_true-unreach-call.cil.c:7200: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-65LBpG/linux-3.14__linux-kernel-locking-mutex__drivers-net-fddi-skfp-skfp_true-unreach-call.cil.c:7201: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-65LBpG/linux-3.14__linux-kernel-locking-mutex__drivers-net-fddi-skfp-skfp_true-unreach-call.cil.c:7202: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-65LBpG/linux-3.14__linux-kernel-locking-mutex__drivers-net-fddi-skfp-skfp_true-unreach-call.cil.c:7205: 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
