bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i


--------------------------------------------------------------------------------


5.0.0-KLEE:86e6f6f8-dg:03407af1-symbiotic:a8aa8ad6-minisat:3db58943-stp:17249213-sbt-instrumentation:dd7e4312
INFO: After compilation stats: Globals/Functions/Blocks/Instr.: 46 128 1371 9718
Removed infinite loop in napi_enable
Removed infinite loop in dma_unmap_page
Removed infinite loop in dma_unmap_single_attrs
Removed infinite loop in dma_map_single_attrs
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 0.511174917221
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'netif_carrier_off' (function is undefined)
Removed calls to 'msleep' (function is undefined)
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'pci_disable_msi' (function is undefined)
Removed calls to 'debug_dma_map_page' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'netif_carrier_on' (function is undefined)
Removed calls to 'debug_dma_unmap_page' (function is undefined)
Removed calls to 'dev_kfree_skb_irq' (function is undefined)
Removed calls to 'consume_skb' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Removed calls to '__const_udelay' (function is undefined)
Defining function dev_warn as symbolic
Defining function _dev_info as symbolic
Defining function dev_err as symbolic
Defining function printk as symbolic
Defining function pci_enable_msi_block as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to '__napi_schedule' (function is undefined)
Removed calls to '__netif_schedule' (function is undefined)
Defining function request_threaded_irq as symbolic
Defining function schedule_work as symbolic
Defining function netpoll_trap as symbolic
Defining function dev_alloc_skb as symbolic
Defining function __phys_addr as symbolic
Removed calls to 'synchronize_irq' (function is undefined)
Defining function crc32_le as symbolic
Defining function del_timer_sync as symbolic
Defining function ethtool_op_get_link as symbolic
Defining function device_set_wakeup_enable as symbolic
Defining function strlcpy as symbolic
Defining function ldv_undefined_int as symbolic
Removed calls to 'get_random_bytes' (function is undefined)
Removed calls to 'ldv_initialize' (function is undefined)
Linked our definitions to these undefined functions:
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 0.371912956238
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 94 70 601 4788
INFO: Starting verification
KLEE: WARNING ONCE: function "atl1c_reinit_locked" has inline asm
KLEE: WARNING ONCE: function "atl1c_irq_disable" has inline asm
KLEE: WARNING ONCE: function "atl1c_stop_mac" has inline asm
KLEE: WARNING ONCE: function "atl1c_wait_until_idle" has inline asm
KLEE: WARNING ONCE: function "atl1c_irq_enable" has inline asm
KLEE: WARNING ONCE: function "atl1c_intr" has inline asm
KLEE: WARNING ONCE: function "atl1c_read_phy_reg" has inline asm
KLEE: WARNING ONCE: function "atl1c_set_aspm" has inline asm
KLEE: WARNING ONCE: function "atl1c_phy_reset" has inline asm
KLEE: WARNING ONCE: function "atl1c_write_phy_reg" has inline asm
KLEE: WARNING ONCE: function "atl1c_set_settings" has inline asm
KLEE: WARNING ONCE: function "atl1c_get_regs" has inline asm
KLEE: WARNING ONCE: function "atl1c_check_eeprom_exist" has inline asm
KLEE: WARNING ONCE: function "atl1c_read_eeprom" has inline asm
KLEE: WARNING ONCE: function "atl1c_hash_set" has inline asm
KLEE: WARNING ONCE: function "atl1c_hw_set_mac_addr" has inline asm
KLEE: WARNING ONCE: function "atl1c_read_mac_addr" has inline asm
KLEE: WARNING ONCE: function "atl1c_phy_disable" has inline asm
KLEE: ERROR: /tmp/symbiotic-mojQvz/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i:5107: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mojQvz/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i:13696: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mojQvz/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i:13021: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mojQvz/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i:13021: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mojQvz/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i:13656: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mojQvz/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i:13656: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mojQvz/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i:13657: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mojQvz/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i:12872: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mojQvz/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i:12872: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mojQvz/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i:13559: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mojQvz/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i:11579: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mojQvz/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i:12874: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mojQvz/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i:11583: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mojQvz/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i:13659: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: (location information missing) memory error: object read only
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: (location information missing) 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-mojQvz/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i:13701: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mojQvz/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i:13701: 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: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mojQvz/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i:13636: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mojQvz/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i:5089: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mojQvz/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i:12824: 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: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mojQvz/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i:5292: inline assembly is unsupported
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-mojQvz/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i:12879: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mojQvz/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i:5374: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mojQvz/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i:12880: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mojQvz/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i:12881: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mojQvz/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i:12882: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mojQvz/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i:12883: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mojQvz/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i:12884: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mojQvz/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i:13638: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mojQvz/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i:13638: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mojQvz/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i:13713: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mojQvz/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i:13639: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mojQvz/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i:13641: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mojQvz/module_get_put-drivers-net-atl1c-atl1c.ko_true-unreach-call.cil.out.i.pp.i:12857: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
