bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--atm--fore_200e.ko_false-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.: 152 589 2465 16364
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_linux_kernel_module_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 0.655827999115
Removed calls to 'ldv_after_alloc' (function is undefined)
Removed calls to 'pci_set_master' (function is undefined)
Removed calls to 'release_firmware' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'tasklet_init' (function is undefined)
Removed calls to 'pci_disable_device' (function is undefined)
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'atm_dev_deregister' (function is undefined)
Defining function printk as symbolic
Defining function msecs_to_jiffies as symbolic
Defining function sprintf as symbolic
Defining function pci_enable_device as symbolic
Removed calls to '__tasklet_schedule' (function is undefined)
Removed calls to '__ldv_linux_kernel_locking_spinlock_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'panic' (function is undefined)
Removed calls to '__dev_kfree_skb_any' (function is undefined)
Defining function skb_put as symbolic
Defining function atm_charge as symbolic
Defining function ktime_get_with_offset as symbolic
Defining function external_allocated_data as symbolic
Defining function request_threaded_irq as symbolic
Defining function request_firmware as symbolic
Defining function atm_dev_register as symbolic
Removed calls to 'might_fault' (function is undefined)
Defining function capable as symbolic
Defining function _copy_to_user as symbolic
Removed calls to '__const_udelay' (function is undefined)
Defining function dma_set_mask as symbolic
Defining function dma_supported as symbolic
Removed calls to 'debug_dma_map_page' (function is undefined)
Removed calls to 'debug_dma_unmap_page' (function is undefined)
Removed calls to 'debug_dma_sync_single_for_cpu' (function is undefined)
Removed calls to 'debug_dma_sync_single_for_device' (function is undefined)
Removed calls to 'debug_dma_alloc_coherent' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
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 __phys_addr 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_assert' (function is undefined)
Linked our definitions to these undefined functions:
  strcmp
  __memcpy
  __memset
  kfree
  __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: 0.669855117798
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 303 511 1879 9026
INFO: Starting verification
KLEE: WARNING ONCE: function "fore200e_open" has inline asm
KLEE: WARNING ONCE: function "fore200e_close" has inline asm
KLEE: WARNING ONCE: function "fore200e_ioctl" has inline asm
KLEE: WARNING ONCE: function "fore200e_change_qos" has inline asm
KLEE: WARNING ONCE: function "fore200e_poll" has inline asm
KLEE: WARNING ONCE: function "fore200e_pca_read" has inline asm
KLEE: WARNING ONCE: function "fore200e_pca_write" has inline asm
KLEE: WARNING ONCE: function "fore200e_pca_dma_map" has inline asm
KLEE: WARNING ONCE: function "fore200e_pca_dma_unmap" has inline asm
KLEE: WARNING ONCE: function "fore200e_pca_dma_sync_for_cpu" has inline asm
KLEE: WARNING ONCE: function "fore200e_pca_dma_sync_for_device" has inline asm
KLEE: WARNING ONCE: function "fore200e_pca_dma_chunk_free" has inline asm
KLEE: WARNING ONCE: function "fore200e_pca_reset" has inline asm
KLEE: WARNING ONCE: function "fore200e_pca_irq_check" has inline asm
KLEE: WARNING ONCE: function "fore200e_pca_irq_ack" has inline asm
KLEE: WARNING ONCE: function "ldv_struct_fore200e_bus_dummy_resourceless_instance_3" has inline asm
KLEE: WARNING ONCE: function "ldv_dummy_resourceless_instance_callback_3_35" has inline asm
KLEE: WARNING ONCE: function "ldv_dummy_resourceless_instance_callback_3_30" has inline asm
KLEE: WARNING ONCE: function "ldv_dummy_resourceless_instance_callback_3_24" has inline asm
KLEE: WARNING ONCE: function "ldv_dummy_resourceless_instance_callback_3_23" 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_8fbdd5ab-359c-4aaf-88b2-7a7367590cb3/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-TvKc_t/linux-4.0-rc1---drivers--atm--fore_200e.ko_false-unreach-call.cil.c:8781: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-TvKc_t/linux-4.0-rc1---drivers--atm--fore_200e.ko_false-unreach-call.cil.c:8723: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-TvKc_t/linux-4.0-rc1---drivers--atm--fore_200e.ko_false-unreach-call.cil.c:7530: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-TvKc_t/linux-4.0-rc1---drivers--atm--fore_200e.ko_false-unreach-call.cil.c:8710: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-TvKc_t/linux-4.0-rc1---drivers--atm--fore_200e.ko_false-unreach-call.cil.c:8746: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-TvKc_t/linux-4.0-rc1---drivers--atm--fore_200e.ko_false-unreach-call.cil.c:7539: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-TvKc_t/linux-4.0-rc1---drivers--atm--fore_200e.ko_false-unreach-call.cil.c:8677: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-TvKc_t/linux-4.0-rc1---drivers--atm--fore_200e.ko_false-unreach-call.cil.c:7530: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-TvKc_t/linux-4.0-rc1---drivers--atm--fore_200e.ko_false-unreach-call.cil.c:8798: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-TvKc_t/linux-4.0-rc1---drivers--atm--fore_200e.ko_false-unreach-call.cil.c:8651: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-TvKc_t/linux-4.0-rc1---drivers--atm--fore_200e.ko_false-unreach-call.cil.c:8710: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-TvKc_t/linux-4.0-rc1---drivers--atm--fore_200e.ko_false-unreach-call.cil.c:8799: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-TvKc_t/linux-4.0-rc1---drivers--atm--fore_200e.ko_false-unreach-call.cil.c:8735: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-TvKc_t/linux-4.0-rc1---drivers--atm--fore_200e.ko_false-unreach-call.cil.c:7539: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-TvKc_t/linux-4.0-rc1---drivers--atm--fore_200e.ko_false-unreach-call.cil.c:7645: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-TvKc_t/linux-4.0-rc1---drivers--atm--fore_200e.ko_false-unreach-call.cil.c:8690: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-TvKc_t/linux-4.0-rc1---drivers--atm--fore_200e.ko_false-unreach-call.cil.c:8690: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-TvKc_t/linux-4.0-rc1---drivers--atm--fore_200e.ko_false-unreach-call.cil.c:7789: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-TvKc_t/linux-4.0-rc1---drivers--atm--fore_200e.ko_false-unreach-call.cil.c:8664: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_8fbdd5ab-359c-4aaf-88b2-7a7367590cb3/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_8fbdd5ab-359c-4aaf-88b2-7a7367590cb3/symbiotic/lib/verifier/__VERIFIER_error.c
Line: 9
assembly.ll line: 1015
Stack: 
	#000001015 in __VERIFIER_error () at /tmp/vcloud-vcloud-master/worker/working_dir_8fbdd5ab-359c-4aaf-88b2-7a7367590cb3/symbiotic/lib/verifier/__VERIFIER_error.c:9
	#100007412 in ldv_struct_fore200e_bus_dummy_resourceless_instance_3 (=0) at /tmp/symbiotic-TvKc_t/linux-4.0-rc1---drivers--atm--fore_200e.ko_false-unreach-call.cil.c:19446
	#200007841 in ldv_entry_EMGentry_9 (=0) at /tmp/symbiotic-TvKc_t/linux-4.0-rc1---drivers--atm--fore_200e.ko_false-unreach-call.cil.c:12085
	#300008683 in main () at /tmp/symbiotic-TvKc_t/linux-4.0-rc1---drivers--atm--fore_200e.ko_false-unreach-call.cil.c:12351

 --- ----------- ---
Generating witness: /tmp/vcloud-vcloud-master/worker/working_dir_8fbdd5ab-359c-4aaf-88b2-7a7367590cb3/symbiotic/witness.graphml
 -- ---- --
Symbolic objects:
nondet := len 1 bytes, |0x0|
nondet:1 := len 8 bytes, |8 times 0x0|
nondet:2 := len 8 bytes, |8 times 0x0|
nondet:3 := len 8 bytes, |8 times 0x0|
nondet:4 := len 4 bytes, |4 times 0x0|
nondet:5 := len 8 bytes, |8 times 0x0|
nondet:6 := len 1 bytes, |0x0|
nondet:7 := len 8 bytes, |8 times 0x0|
nondet:8 := len 8 bytes, |8 times 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 8 bytes, |8 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 8 bytes, |8 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 4 bytes, |4 times 0x0|
nondet:28 := len 4 bytes, |4 times 0x0|
nondet:29 := len 8 bytes, |8 times 0x0|
nondet:30 := len 8 bytes, |8 times 0x0|
nondet:31 := len 4 bytes, |4 times 0x0|
nondet:32 := len 4 bytes, |4 times 0x0|
nondet:33 := len 36 bytes, |36 times 0x0|
nondet:34 := len 2 bytes, |2 times 0x0|
nondet:35 := len 8 bytes, |8 times 0x0|
nondet:36 := len 8 bytes, |8 times 0x0|
nondet:37 := len 8 bytes, |8 times 0x0|
nondet:38 := len 8 bytes, |8 times 0x0|
nondet:39 := len 8 bytes, |8 times 0x0|
nondet:40 := len 8 bytes, |8 times 0x0|
nondet:41 := len 8 bytes, |8 times 0x0|
nondet:42 := len 8 bytes, |8 times 0x0|
nondet:43 := len 8 bytes, |8 times 0x0|
nondet:44 := len 8 bytes, |8 times 0x0|
nondet:45 := len 8 bytes, |8 times 0x0|
nondet:46 := len 8 bytes, |8 times 0x0|
nondet:47 := len 8 bytes, |8 times 0x0|
nondet:48 := len 8 bytes, |8 times 0x0|
nondet:49 := len 8 bytes, |8 times 0x0|
nondet:50 := len 8 bytes, |8 times 0x0|
nondet:51 := len 8 bytes, |8 times 0x0|
nondet:52 := len 8 bytes, |8 times 0x0|
nondet:53 := len 8 bytes, |8 times 0x0|
nondet:54 := len 8 bytes, |8 times 0x0|
nondet:55 := len 1 bytes, |0x0|
nondet:56 := len 8 bytes, |8 times 0x0|
nondet:57 := len 8 bytes, |8 times 0x0|
nondet:58 := len 8 bytes, |8 times 0x0|
nondet:59 := len 8 bytes, |8 times 0x0|
nondet:60 := len 8 bytes, |8 times 0x0|
nondet:61 := len 8 bytes, |8 times 0x0|
nondet:62 := len 8 bytes, |8 times 0x0|
nondet:63 := len 8 bytes, |8 times 0x0|
nondet:64 := len 8 bytes, |8 times 0x0|
nondet:65 := len 8 bytes, |8 times 0x0|
nondet:66 := len 8 bytes, |8 times 0x0|
nondet:67 := len 8 bytes, |8 times 0x0|
nondet:68 := len 4 bytes, |4 times 0x0|
nondet:69 := len 8 bytes, |0xb8|0x78|0x32|0x3|4 times 0x0|
extern-global:nr_cpu_ids := len 4 bytes, |3 times 0xff|0x7f|
extern-global:__this_module := len 856 bytes, |856 times 0x0|
extern-global:x86_dma_fallback_dev := len 1416 bytes, |1416 times 0x0|
extern-global:dma_ops := len 128 bytes, |128 times 0x0|
extern-global:pv_irq_ops := len 56 bytes, |56 times 0x0|
extern-global:jiffies := len 8 bytes, |0x1|7 times 0x0|
ldv_undef_int:tmp:16037 := len 4 bytes, |4 times 0x1|
malloc0 := len 16 bytes, |16 times 0x0|
malloc0:1 := len 2968 bytes, |2968 times 0x0|
malloc0:2 := len 32 bytes, |32 times 0x0|
ldv_undef_int:tmp:16037:1 := len 4 bytes, |4 times 0x0|
ldv_undef_int:tmp:16037:2 := len 4 bytes, |4 times 0x0|
ldv_undef_int:tmp:16037:3 := len 4 bytes, |4 times 0x1|
malloc0:3 := len 4 bytes, |4 times 0x0|
ldv_undef_int:tmp:16037:4 := len 4 bytes, |0x2|3 times 0x0|
 -- ---- --
INFO: Total time elapsed: 64.148170948
