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-sis900.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.: 77 118 1208 8126
Removed infinite loop in dma_unmap_single_attrs
Removed infinite loop in dma_map_single_attrs
Removed infinite loop in arch_local_save_flags
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 0.353963851929
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'ldv_check_return_value' (function is undefined)
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Removed calls to 'pci_unregister_driver' (function is undefined)
Removed calls to 'init_timer_key' (function is undefined)
Removed calls to 'add_timer' (function is undefined)
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'consume_skb' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'netif_carrier_off' (function is undefined)
Removed calls to 'dev_kfree_skb_irq' (function is undefined)
Removed calls to 'disable_irq' (function is undefined)
Removed calls to 'enable_irq' (function is undefined)
Removed calls to 'pci_set_master' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Removed calls to 'pci_dev_put' (function is undefined)
Removed calls to 'get_random_bytes' (function is undefined)
Removed calls to 'yield' (function is undefined)
Removed calls to 'netif_carrier_on' (function is undefined)
Removed calls to 'pci_release_regions' (function is undefined)
Removed calls to 'free_netdev' (function is undefined)
Removed calls to 'netif_device_detach' (function is undefined)
Removed calls to 'pci_restore_state' (function is undefined)
Removed calls to 'netif_device_attach' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function printk as symbolic
Removed calls to 'debug_dma_unmap_page' (function is undefined)
Removed calls to '__netif_schedule' (function is undefined)
Defining function netpoll_trap as symbolic
Defining function dev_alloc_skb as symbolic
Defining function skb_put as symbolic
Defining function eth_type_trans as symbolic
Defining function netif_rx as symbolic
Removed calls to 'debug_dma_map_page' (function is undefined)
Defining function __phys_addr as symbolic
Defining function pci_set_power_state as symbolic
Defining function dev_get_drvdata as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function pci_save_state as symbolic
Defining function pci_enable_device as symbolic
Defining function alloc_etherdev_mqs as symbolic
Defining function pci_request_regions as symbolic
Removed calls to 'debug_dma_alloc_coherent' (function is undefined)
Defining function pci_get_device as symbolic
Defining function register_netdev as symbolic
Removed calls to 'debug_dma_free_coherent' (function is undefined)
Defining function pci_bus_write_config_byte as symbolic
Defining function pci_bus_read_config_byte as symbolic
Defining function dev_set_drvdata as symbolic
Defining function dma_set_mask as symbolic
Defining function pci_bus_write_config_dword as symbolic
Defining function pci_bus_read_config_dword as symbolic
Defining function mii_nway_restart as symbolic
Defining function mii_ethtool_sset as symbolic
Defining function mii_ethtool_gset as symbolic
Defining function mii_link_ok as symbolic
Defining function _raw_spin_lock_irqsave as symbolic
Defining function crc32_le as symbolic
Defining function bitrev32 as symbolic
Defining function del_timer as symbolic
Defining function request_threaded_irq as symbolic
Defining function __pci_register_driver as symbolic
Removed calls to 'unregister_netdev' (function is undefined)
Defining function eth_mac_addr as symbolic
Defining function eth_validate_addr as symbolic
Defining function eth_change_mtu as symbolic
Defining function ldv_undefined_int as symbolic
Linked our definitions to these undefined functions:
  strcpy
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 0.323566913605
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 142 90 571 4051
INFO: Starting verification
KLEE: WARNING ONCE: function "sis900_open" has inline asm
KLEE: WARNING ONCE: function "sis900_close" has inline asm
KLEE: WARNING ONCE: function "sis900_start_xmit" has inline asm
KLEE: WARNING ONCE: function "set_rx_mode" has inline asm
KLEE: WARNING ONCE: function "sis900_tx_timeout" has inline asm
KLEE: WARNING ONCE: function "sis900_get_wol" has inline asm
KLEE: WARNING ONCE: function "sis900_set_wol" has inline asm
KLEE: WARNING ONCE: function "sis900_probe" has inline asm
KLEE: WARNING ONCE: function "sis900_suspend" has inline asm
KLEE: WARNING ONCE: function "sis900_resume" has inline asm
KLEE: WARNING ONCE: function "sis900_interrupt" has inline asm
KLEE: WARNING ONCE: function "sis900_timer" has inline asm
KLEE: WARNING ONCE: function "mdio_read" has inline asm
KLEE: WARNING ONCE: function "sis900_check_mode" has inline asm
KLEE: WARNING ONCE: function "mdio_write" 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 "netif_wake_queue" has inline asm
KLEE: WARNING ONCE: function "sis900_init_rxfilter" has inline asm
KLEE: WARNING ONCE: function "sis900_init_tx_ring" has inline asm
KLEE: WARNING ONCE: function "sis900_init_rx_ring" has inline asm
KLEE: WARNING ONCE: function "netif_stop_queue" has inline asm
KLEE: WARNING ONCE: function "read_eeprom" has inline asm
KLEE: WARNING ONCE: function "pci_free_consistent" has inline asm
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:7996: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:7996: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:7454: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:8249: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:8297: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:8071: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:8590: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:8624: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:4464: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:7535: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:8364: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:8075: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:4464: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:8130: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:8252: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:7454: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:7379: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:7452: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:4618: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:4610: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:8589: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:7381: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:4618: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:8077: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:7275: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:4618: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:7044: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:5722: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:5722: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:8219: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:4670: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:6649: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:4610: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:8384: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:8225: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:4610: inline assembly is unsupported
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: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:4618: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:4439: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:6630: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:5113: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:7467: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:8216: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:7465: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:5753: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:5753: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:8219: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_a637f236-d81b-4b1e-a807-d40f314a529d/symbiotic/lib/verifier/__VERIFIER_error.c:9: ASSERTION FAIL: verifier assertion failed
KLEE: NOTE: now ignoring this error at this location
Error found.
RESULT: false(unreach-call)

 --- Error trace ---

Error: ASSERTION FAIL: verifier assertion failed
File: /tmp/vcloud-vcloud-master/worker/working_dir_a637f236-d81b-4b1e-a807-d40f314a529d/symbiotic/lib/verifier/__VERIFIER_error.c
Line: 9
assembly.ll line: 549
Stack: 
	#000000549 in __VERIFIER_error () at /tmp/vcloud-vcloud-master/worker/working_dir_a637f236-d81b-4b1e-a807-d40f314a529d/symbiotic/lib/verifier/__VERIFIER_error.c:9
	#100003533 in ldv_blast_assert () at /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:8987
	#200000924 in main () at /tmp/symbiotic-BOCWG1/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i.pp.i:9067

 --- ----------- ---
Generating witness: /tmp/vcloud-vcloud-master/worker/working_dir_a637f236-d81b-4b1e-a807-d40f314a529d/symbiotic/witness.graphml
 -- ---- --
Symbolic objects:
nondet := len 8 bytes, |8 times 0x0|
nondet:1 := len 8 bytes, |8 times 0x0|
nondet:2 := len 8 bytes, |8 times 0x0|
nondet:3 := len 2 bytes, |2 times 0x0|
nondet:4 := len 8 bytes, |8 times 0x0|
nondet:5 := len 8 bytes, |8 times 0x0|
nondet:6 := len 4 bytes, |4 times 0x0|
nondet:7 := len 8 bytes, |8 times 0x0|
nondet:8 := len 1 bytes, |0x0|
nondet:9 := len 8 bytes, |8 times 0x0|
nondet:10 := len 8 bytes, |8 times 0x0|
nondet:11 := len 8 bytes, |8 times 0x0|
nondet:12 := len 8 bytes, |8 times 0x0|
nondet:13 := len 8 bytes, |8 times 0x0|
nondet:14 := len 2 bytes, |2 times 0x0|
nondet:15 := len 8 bytes, |8 times 0x0|
nondet:16 := len 8 bytes, |8 times 0x0|
nondet:17 := len 8 bytes, |8 times 0x0|
nondet:18 := len 8 bytes, |8 times 0x0|
nondet:19 := len 4 bytes, |4 times 0x0|
nondet:20 := len 8 bytes, |8 times 0x0|
nondet:21 := len 8 bytes, |8 times 0x0|
nondet:22 := len 8 bytes, |8 times 0x0|
nondet:23 := len 8 bytes, |8 times 0x0|
nondet:24 := len 8 bytes, |8 times 0x0|
nondet:25 := len 8 bytes, |8 times 0x0|
nondet:26 := len 8 bytes, |8 times 0x0|
nondet:27 := len 8 bytes, |8 times 0x0|
nondet:28 := len 4 bytes, |4 times 0x0|
nondet:29 := len 8 bytes, |0xe4|0x33|0x51|0x2|4 times 0x0|
extern-global:__this_module := len 608 bytes, |608 times 0x0|
extern-global:x86_dma_fallback_dev := len 1112 bytes, |1112 times 0x0|
extern-global:pv_irq_ops := len 56 bytes, |56 times 0x0|
extern-global:dma_ops := len 112 bytes, |112 times 0x0|
extern-global:jiffies := len 8 bytes, |8 times 0x0|
main:tmp___1:8958 := len 4 bytes, |4 times 0x1|
main:tmp___0:8734 := len 4 bytes, |0xa|3 times 0x0|
main:tmp___1:8958:1 := len 4 bytes, |4 times 0x0|
 -- ---- --
INFO: Total time elapsed: 559.730057955
