bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--ethernet--sfc--sfc.ko-ldv_main0_sequence_infinite_withcheck_stateful.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.: 762 1276 10816 75559
Removed infinite loop in falcon_probe_nic
Removed infinite loop in falcon_remove_nic
Removed infinite loop in falcon_monitor
Removed infinite loop in falcon_reconfigure_port
Removed infinite loop in efx_start_interrupts
Removed infinite loop in efx_start_all
Removed infinite loop in efx_start_port
Removed infinite loop in efx_sriov_reset_vf
Removed infinite loop in arch_local_save_flags
Removed infinite loop in efx_mcdi_rpc_start
Removed infinite loop in efx_mcdi_rpc_finish
Removed infinite loop in efx_mcdi_copyout
Removed infinite loop in efx_mcdi_copyin
Removed infinite loop in efx_filter_build
Removed infinite loop in napi_enable
Removed infinite loop in efx_stop_datapath
Removed infinite loop in dma_unmap_single_attrs
Removed infinite loop in dma_unmap_page
Removed infinite loop in dma_unmap_page___0
Removed infinite loop in dma_unmap_single_attrs___0
Removed infinite loop in siena_probe_nic
Removed infinite loop in efx_filter_insert_filter
Removed infinite loop in efx_test_loopbacks
Removed infinite loop in efx_process_channel_now
Removed infinite loop in dma_map_single_attrs___0
Removed infinite loop in dma_map_page___0
Removed infinite loop in get_page
Removed infinite loop in efx_loopback_rx_packet
Removed infinite loop in efx_sriov_reset_rx_filter
Removed infinite loop in dma_map_single_attrs
Removed infinite loop in efx_nic_push_buffers
Removed infinite loop in dql_queued
Removed infinite loop in dma_map_page
Removed infinite loop in napi_enable___0
Removed infinite loop in efx_alloc_special_buffer
Removed infinite loop in efx_sriov_fini
Removed infinite loop in efx_unregister_netdev
Removed infinite loop in efx_pci_remove_main
Removed infinite loop in efx_sriov_peer_work
Removed infinite loop in efx_monitor
Removed infinite loop in efx_sriov_reset_tx_filter
Removed infinite loop in efx_ptp_rx
INFO: Compilation, preparation and instrumentation time: 2.84905695915
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'init_timer_key' (function is undefined)
Removed calls to 'pci_dev_put' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'msleep' (function is undefined)
Removed calls to '_raw_spin_lock_bh' (function is undefined)
Removed calls to '_raw_spin_unlock_bh' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function netdev_err as symbolic
Removed calls to '__const_udelay' (function is undefined)
Defining function _cond_resched as symbolic
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Defining function schedule_timeout_uninterruptible as symbolic
Removed calls to 'dump_stack' (function is undefined)
Defining function rtnl_is_locked as symbolic
Defining function printk as symbolic
Defining function queue_delayed_work as symbolic
Removed calls to 'netif_carrier_on' (function is undefined)
Removed calls to 'netif_carrier_off' (function is undefined)
Defining function netdev_info as symbolic
Removed calls to '__netif_schedule' (function is undefined)
Defining function netpoll_trap as symbolic
Removed calls to 'debug_dma_free_coherent' (function is undefined)
Defining function net_ratelimit as symbolic
Removed calls to 'prepare_to_wait' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Defining function queue_work as symbolic
Defining function autoremove_wake_function as symbolic
Defining function schedule_timeout as symbolic
Removed calls to 'schedule' (function is undefined)
Removed calls to 'debug_dma_alloc_coherent' (function is undefined)
Removed calls to 'local_bh_disable' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'local_bh_enable' (function is undefined)
Removed calls to 'synchronize_irq' (function is undefined)
Removed calls to 'dql_reset' (function is undefined)
Removed calls to 'dev_kfree_skb_any' (function is undefined)
Removed calls to 'debug_dma_unmap_page' (function is undefined)
Defining function del_timer_sync as symbolic
Removed calls to '__free_pages' (function is undefined)
Defining function msecs_to_jiffies as symbolic
Defining function cancel_delayed_work_sync as symbolic
Defining function cancel_work_sync as symbolic
Defining function pci_wake_from_d3 as symbolic
Defining function __phys_addr as symbolic
Removed calls to 'device_remove_file' (function is undefined)
Removed calls to 'hwmon_device_unregister' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Defining function hwmon_device_register as symbolic
Defining function snprintf as symbolic
Defining function sprintf as symbolic
Defining function dev_get_drvdata as symbolic
Defining function strlcpy as symbolic
Defining function device_create_file as symbolic
Defining function ethtool_op_get_link as symbolic
Defining function ptp_clock_index as symbolic
Removed calls to 'pci_set_master' (function is undefined)
Removed calls to 'netif_device_attach' (function is undefined)
Removed calls to 'netif_device_detach' (function is undefined)
Defining function dev_close as symbolic
Defining function dev_open as symbolic
Removed calls to 'put_page' (function is undefined)
Removed calls to 'debug_dma_map_page' (function is undefined)
Defining function mod_timer as symbolic
Removed calls to 'debug_dma_mapping_error' (function is undefined)
Defining function __netdev_alloc_skb as symbolic
Defining function __get_page_tail as symbolic
Defining function alloc_pages_current as symbolic
Defining function skb_put as symbolic
Defining function eth_type_trans as symbolic
Defining function netif_receive_skb as symbolic
Defining function napi_get_frags as symbolic
Defining function napi_gro_frags as symbolic
Defining function napi_gro_receive as symbolic
Removed calls to 'list_del' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Defining function netdev_warn as symbolic
Removed calls to 'dql_completed' (function is undefined)
Defining function skb_pad as symbolic
Removed calls to 'netif_napi_add' (function is undefined)
Removed calls to 'netif_napi_del' (function is undefined)
Removed calls to 'napi_complete' (function is undefined)
Defining function rps_may_expire_flow as symbolic
Defining function _raw_spin_trylock_bh as symbolic
Defining function mdio45_nway_restart as symbolic
Removed calls to 'mdio45_ethtool_gset_npage' (function is undefined)
Defining function mdio_set_flag as symbolic
Defining function mdio45_links_ok as symbolic
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to 'pci_release_region' (function is undefined)
Removed calls to 'pci_disable_device' (function is undefined)
Removed calls to '__bitmap_or' (function is undefined)
Removed calls to 'free_cpumask_var' (function is undefined)
Removed calls to 'free_irq_cpu_rmap' (function is undefined)
Removed calls to 'get_random_bytes' (function is undefined)
Removed calls to 'pci_disable_msix' (function is undefined)
Removed calls to 'rtnl_lock' (function is undefined)
Removed calls to 'rtnl_unlock' (function is undefined)
Removed calls to 'unregister_netdevice_queue' (function is undefined)
Removed calls to 'free_netdev' (function is undefined)
Removed calls to 'pci_disable_sriov' (function is undefined)
Removed calls to 'iounmap' (function is undefined)
Removed calls to 'destroy_workqueue' (function is undefined)
Defining function dev_set_drvdata as symbolic
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'vfree' (function is undefined)
Removed calls to 'pci_disable_msi' (function is undefined)
Defining function mtd_device_unregister as symbolic
Defining function alloc_etherdev_mqs as symbolic
Removed calls to 'mtd_erase_callback' (function is undefined)
Defining function mtd_device_parse_register as symbolic
Defining function pci_enable_sriov as symbolic
Defining function pci_find_ext_capability as symbolic
Defining function pci_bus_read_config_word as symbolic
Defining function dev_alloc_name as symbolic
Defining function register_netdevice as symbolic
Removed calls to 'pci_clear_master' (function is undefined)
Removed calls to '__napi_schedule' (function is undefined)
Defining function request_threaded_irq as symbolic
Defining function vzalloc as symbolic
Defining function netif_set_real_num_tx_queues as symbolic
Defining function netif_set_real_num_rx_queues as symbolic
Defining function pci_enable_msix as symbolic
Defining function pci_enable_msi_block as symbolic
Defining function irq_cpu_rmap_add as symbolic
Defining function alloc_cpu_rmap as symbolic
Defining function zalloc_cpumask_var as symbolic
Defining function find_next_bit as symbolic
Defining function pci_enable_device as symbolic
Defining function dma_supported as symbolic
Defining function dma_set_mask as symbolic
Defining function pci_request_region as symbolic
Defining function ioremap_nocache as symbolic
Defining function pci_read_vpd as symbolic
Defining function pci_vpd_find_tag as symbolic
Defining function pci_vpd_find_info_keyword as symbolic
Defining function __alloc_workqueue_key as symbolic
Defining function mutex_trylock as symbolic
Removed calls to 'pci_restore_state' (function is undefined)
Defining function pci_save_state as symbolic
Defining function pci_set_power_state as symbolic
Defining function eth_validate_addr as symbolic
Removed calls to 'might_fault' (function is undefined)
Defining function mdio_mii_ioctl as symbolic
Defining function _copy_to_user as symbolic
Removed calls to 'skb_queue_purge' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Defining function skb_dequeue as symbolic
Defining function _copy_from_user as symbolic
Defining function crc32_le as symbolic
Removed calls to 'skb_queue_tail' (function is undefined)
Defining function schedule_delayed_work as symbolic
Removed calls to 'i2c_unregister_device' (function is undefined)
Defining function i2c_smbus_read_byte_data as symbolic
Defining function i2c_new_device as symbolic
Defining function i2c_smbus_write_byte_data as symbolic
Defining function i2c_new_dummy as symbolic
Defining function ptp_clock_unregister as symbolic
Removed calls to 'skb_queue_head' (function is undefined)
Removed calls to 'skb_tstamp_tx' (function is undefined)
Removed calls to 'consume_skb' (function is undefined)
Removed calls to 'set_normalized_timespec' (function is undefined)
Defining function ptp_clock_register as symbolic
Removed calls to 'getnstimeofday' (function is undefined)
Removed calls to 'ptp_clock_event' (function is undefined)
Defining function ns_to_timespec as symbolic
Defining function skb_checksum_help as symbolic
Defining function __pskb_pull_tail as symbolic
Defining function mutex_lock_interruptible as symbolic
Defining function round_jiffies_up as symbolic
Defining function i2c_del_adapter as symbolic
Defining function pci_dev_get as symbolic
Defining function pci_get_device as symbolic
Defining function i2c_bit_add_bus 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 unregister_netdevice_notifier as symbolic
Defining function register_netdevice_notifier as symbolic
Defining function __pci_register_driver as symbolic
Linked our definitions to these undefined functions:
  memcmp
  strchr
  strcpy
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 2.67927002907
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 992 959 5773 41736
INFO: Starting verification
KLEE: WARNING ONCE: function "falcon_probe_nic" has inline asm
KLEE: WARNING ONCE: function "falcon_remove_nic" has inline asm
KLEE: WARNING ONCE: function "falcon_monitor" has inline asm
KLEE: WARNING ONCE: function "falcon_handle_global_event" has inline asm
KLEE: WARNING ONCE: function "falcon_update_nic_stats" has inline asm
KLEE: WARNING ONCE: function "falcon_spi_read" has inline asm
KLEE: WARNING ONCE: function "efx_reado" has inline asm
KLEE: WARNING ONCE: function "efx_writeo" has inline asm
KLEE: WARNING ONCE: function "falcon_b0_test_chip" has inline asm
KLEE: WARNING ONCE: function "efx_start_interrupts" has inline asm
KLEE: WARNING ONCE: function "efx_restore_filters" has inline asm
KLEE: WARNING ONCE: function "efx_start_all" has inline asm
KLEE: WARNING ONCE: function "netif_tx_wake_queue" has inline asm
KLEE: WARNING ONCE: function "efx_nic_init_rx" has inline asm
KLEE: WARNING ONCE: function "efx_init_special_buffer" has inline asm
KLEE: WARNING ONCE: function "efx_nic_init_tx" has inline asm
KLEE: WARNING ONCE: function "efx_sriov_reset_vf" has inline asm
KLEE: WARNING ONCE: function "dma_free_attrs" has inline asm
KLEE: WARNING ONCE: function "efx_sriov_memcpy" has inline asm
KLEE: WARNING ONCE: function "efx_sriov_bufs" has inline asm
KLEE: WARNING ONCE: function "efx_mcdi_rpc_start" has inline asm
KLEE: WARNING ONCE: function "efx_mcdi_rpc_finish" has inline asm
KLEE: WARNING ONCE: function "efx_mcdi_poll" has inline asm
KLEE: WARNING ONCE: function "efx_schedule_reset" has inline asm
KLEE: WARNING ONCE: function "efx_mcdi_poll_reboot" has inline asm
KLEE: WARNING ONCE: function "efx_mcdi_complete" has inline asm
KLEE: WARNING ONCE: function "efx_mcdi_acquire" has inline asm
KLEE: WARNING ONCE: function "efx_filter_build" has inline asm
KLEE: WARNING ONCE: function "efx_nic_init_eventq" has inline asm
KLEE: WARNING ONCE: function "efx_start_eventq" has inline asm
KLEE: WARNING ONCE: function "napi_enable" has inline asm
KLEE: WARNING ONCE: function "efx_stop_all" has inline asm
KLEE: WARNING ONCE: function "napi_disable" has inline asm
KLEE: WARNING ONCE: function "netif_tx_stop_queue" has inline asm
KLEE: WARNING ONCE: function "efx_nic_flush_queues" has inline asm
KLEE: WARNING ONCE: function "efx_release_tx_buffers" has inline asm
KLEE: WARNING ONCE: function "efx_mcdi_flush_rxqs" has inline asm
KLEE: WARNING ONCE: function "siena_probe_nic" has inline asm
KLEE: WARNING ONCE: function "siena_update_nic_stats" has inline asm
KLEE: WARNING ONCE: function "_efx_writed_page_locked" has inline asm
KLEE: WARNING ONCE: function "efx_nic_push_rx_indir_table" has inline asm
KLEE: WARNING ONCE: function "efx_mcdi_mon_probe" has inline asm
KLEE: WARNING ONCE: function "efx_device_detach_sync" has inline asm
KLEE: WARNING ONCE: function "efx_filter_insert_filter" has inline asm
KLEE: WARNING ONCE: function "efx_filter_remove_id_safe" has inline asm
KLEE: WARNING ONCE: function "efx_filter_table_clear_entry" has inline asm
KLEE: WARNING ONCE: function "efx_filter_count_rx_used" has inline asm
KLEE: WARNING ONCE: function "efx_filter_get_filter_safe" has inline asm
KLEE: WARNING ONCE: function "efx_filter_get_rx_ids" has inline asm
KLEE: WARNING ONCE: function "efx_selftest" has inline asm
KLEE: WARNING ONCE: function "efx_process_channel_now" has inline asm
KLEE: WARNING ONCE: function "efx_nic_process_eventq" has inline asm
KLEE: WARNING ONCE: function "get_page" has inline asm
KLEE: WARNING ONCE: function "efx_nic_notify_rx_desc" has inline asm
KLEE: WARNING ONCE: function "efx_loopback_rx_packet" has inline asm
KLEE: WARNING ONCE: function "efx_xmit_done" has inline asm
KLEE: WARNING ONCE: function "efx_handle_drain_event" has inline asm
KLEE: WARNING ONCE: function "efx_sriov_tx_flush_done" has inline asm
KLEE: WARNING ONCE: function "efx_sriov_rx_flush_done" has inline asm
KLEE: WARNING ONCE: function "efx_sriov_reset_rx_filter" has inline asm
KLEE: WARNING ONCE: function "efx_probe_channel" has inline asm
KLEE: WARNING ONCE: function "efx_alloc_special_buffer" has inline asm
KLEE: WARNING ONCE: function "efx_probe_tx_queue" has inline asm
KLEE: WARNING ONCE: function "efx_probe_rx_queue" has inline asm
KLEE: WARNING ONCE: function "efx_nic_get_regs" has inline asm
KLEE: WARNING ONCE: function "efx_mdio_test_alive" has inline asm
KLEE: WARNING ONCE: function "efx_mdio_check_mmds" has inline asm
KLEE: WARNING ONCE: function "efx_pci_probe" has inline asm
KLEE: WARNING ONCE: function "efx_pci_remove" has inline asm
KLEE: WARNING ONCE: function "efx_sriov_fini" has inline asm
KLEE: WARNING ONCE: function "efx_pci_remove_main" has inline asm
KLEE: WARNING ONCE: function "efx_nic_fini_interrupt" has inline asm
KLEE: WARNING ONCE: function "efx_reset_work" has inline asm
KLEE: WARNING ONCE: function "efx_monitor" has inline asm
KLEE: WARNING ONCE: function "efx_mtd_probe" has inline asm
KLEE: WARNING ONCE: function "efx_sriov_peer_work" has inline asm
KLEE: WARNING ONCE: function "efx_legacy_interrupt" has inline asm
KLEE: WARNING ONCE: function "falcon_legacy_interrupt_a1" has inline asm
KLEE: WARNING ONCE: function "efx_msi_interrupt" has inline asm
KLEE: WARNING ONCE: function "napi_schedule" has inline asm
KLEE: WARNING ONCE: function "efx_set_rx_mode" has inline asm
KLEE: WARNING ONCE: function "__efx_sriov_update_vf_addr" has inline asm
KLEE: WARNING ONCE: function "netdev_tx_sent_queue" has inline asm
KLEE: WARNING ONCE: function "efx_nic_push_buffers" has inline asm
KLEE: WARNING ONCE: function "efx_tx_maybe_stop_queue" has inline asm
KLEE: WARNING ONCE: function "efx_ptp_rx" has inline asm
KLEE: WARNING ONCE: function "efx_ptp_pps_worker" has inline asm
KLEE: WARNING ONCE: function "falcon_mtd_erase" has inline asm
KLEE: WARNING ONCE: function "efx_spi_slow_wait" has inline asm
KLEE: WARNING ONCE: function "falcon_spi_write" has inline asm
KLEE: WARNING ONCE: function "efx_vfdi_init_evq" has inline asm
KLEE: WARNING ONCE: function "efx_vfdi_init_rxq" has inline asm
KLEE: WARNING ONCE: function "efx_vfdi_init_txq" has inline asm
KLEE: WARNING ONCE: function "efx_vfdi_fini_all_queues" has inline asm
KLEE: WARNING ONCE: function "falcon_stats_complete" has inline asm
KLEE: WARNING ONCE: function "falcon_stats_request" has inline asm
KLEE: WARNING ONCE: function "efx_nic_enable_interrupts" has inline asm
KLEE: WARNING ONCE: function "efx_nic_eventq_read_ack" has inline asm
KLEE: WARNING ONCE: function "__efx_filter_rfs_expire" has inline asm
KLEE: WARNING ONCE: function "falcon_irq_ack_a1" has inline asm
KLEE: WARNING: undefined reference to function: delayed_work_timer_fn
KLEE: WARNING ONCE: flushing 9576 bytes on read, may be slow and/or crash: MO127[9576] allocated at global:
KLEE: ERROR: /tmp/symbiotic-MQVuCa/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--ethernet--sfc--sfc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:11897: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-MQVuCa/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--ethernet--sfc--sfc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:12944: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-MQVuCa/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--ethernet--sfc--sfc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:9016: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-MQVuCa/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--ethernet--sfc--sfc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:11449: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-MQVuCa/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--ethernet--sfc--sfc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:11415: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-MQVuCa/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--ethernet--sfc--sfc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:9017: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-MQVuCa/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--ethernet--sfc--sfc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:11818: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-MQVuCa/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--ethernet--sfc--sfc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:12945: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-MQVuCa/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--ethernet--sfc--sfc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:8353: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-MQVuCa/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--ethernet--sfc--sfc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:11559: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-MQVuCa/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--ethernet--sfc--sfc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:9018: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-MQVuCa/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--ethernet--sfc--sfc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:11860: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-MQVuCa/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--ethernet--sfc--sfc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:11744: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-MQVuCa/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--ethernet--sfc--sfc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:11716: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-MQVuCa/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--ethernet--sfc--sfc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:11825: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-MQVuCa/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--ethernet--sfc--sfc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:34834: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-MQVuCa/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--ethernet--sfc--sfc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:11716: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-MQVuCa/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--ethernet--sfc--sfc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:7716: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-MQVuCa/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--ethernet--sfc--sfc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:7949: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-MQVuCa/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--ethernet--sfc--sfc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:8234: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-MQVuCa/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--net--ethernet--sfc--sfc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:11044: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
