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-atm-eni.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.: 176 111 1744 11023
Removed infinite loop in arch_local_save_flags
Removed infinite loop in dma_map_single_attrs
Removed infinite loop in dma_unmap_single_attrs
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 0.400434017181
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'ldv_check_return_value' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Removed calls to 'add_wait_queue' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'remove_wait_queue' (function is undefined)
Removed calls to 'consume_skb' (function is undefined)
Removed calls to 'skb_queue_tail' (function is undefined)
Removed calls to '__tasklet_schedule' (function is undefined)
Removed calls to '_raw_read_lock' (function is undefined)
Removed calls to '_raw_read_unlock' (function is undefined)
Removed calls to 'debug_dma_alloc_coherent' (function is undefined)
Removed calls to 'iounmap' (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 'tasklet_init' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'free_pages' (function is undefined)
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'atm_dev_deregister' (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 '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function pci_enable_device as symbolic
Defining function atm_dev_register as symbolic
Defining function printk as symbolic
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'skb_queue_head' (function is undefined)
Removed calls to 'dev_kfree_skb_irq' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Defining function get_zeroed_page as symbolic
Defining function _raw_spin_lock_irqsave as symbolic
Defining function skb_dequeue as symbolic
Removed calls to 'debug_dma_map_page' (function is undefined)
Defining function __phys_addr as symbolic
Removed calls to 'debug_dma_unmap_page' (function is undefined)
Defining function ktime_get_real as symbolic
Defining function pci_bus_write_config_byte as symbolic
Defining function pci_bus_write_config_word as symbolic
Defining function request_threaded_irq as symbolic
Defining function ioremap_nocache as symbolic
Defining function suni_init as symbolic
Defining function pci_bus_read_config_byte as symbolic
Defining function dev_set_drvdata as symbolic
Defining function sprintf as symbolic
Defining function atm_pcr_goal as symbolic
Defining function capable as symbolic
Removed calls to 'might_fault' (function is undefined)
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Defining function _copy_from_user as symbolic
Defining function default_wake_function as symbolic
Defining function atm_alloc_charge as symbolic
Defining function skb_put as symbolic
Defining function __pci_register_driver as symbolic
Defining function ldv_undefined_int as symbolic
Linked our definitions to these undefined functions:
  __kmalloc
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 0.416830062866
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 234 64 644 5489
INFO: Starting verification
KLEE: WARNING ONCE: function "main" has inline asm
KLEE: WARNING ONCE: function "eni_open" has inline asm
KLEE: WARNING ONCE: function "eni_close" has inline asm
KLEE: WARNING ONCE: function "eni_send" has inline asm
KLEE: WARNING ONCE: function "eni_change_qos" has inline asm
KLEE: WARNING ONCE: function "eni_init_one" has inline asm
KLEE: WARNING ONCE: function "eni_int" has inline asm
KLEE: WARNING ONCE: function "reserve_or_set_tx" has inline asm
KLEE: WARNING ONCE: function "do_tx" has inline asm
KLEE: WARNING ONCE: function "pci_map_single" has inline asm
KLEE: WARNING ONCE: function "rx_aal5" has inline asm
KLEE: WARNING ONCE: function "rx_aal0" has inline asm
KLEE: WARNING ONCE: function "rx_ident_err" has inline asm
KLEE: WARNING ONCE: function "do_rx_dma" has inline asm
KLEE: WARNING ONCE: function "pci_unmap_single" has inline asm
KLEE: WARNING ONCE: function "eni_phy_put" has inline asm
KLEE: WARNING ONCE: function "eni_phy_get" has inline asm
KLEE: WARNING ONCE: flushing 9608 bytes on read, may be slow and/or crash: MO21[9608] allocated at global:
KLEE: ERROR: /tmp/symbiotic-K5IbmS/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i.pp.i:10277: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-K5IbmS/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i.pp.i:10287: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-K5IbmS/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i.pp.i:10287: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-K5IbmS/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i.pp.i:9908: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-K5IbmS/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i.pp.i:10277: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-K5IbmS/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i.pp.i:9790: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-K5IbmS/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i.pp.i:8828: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-K5IbmS/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i.pp.i:10198: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-K5IbmS/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i.pp.i:9908: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-K5IbmS/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i.pp.i:8829: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-K5IbmS/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i.pp.i:5347: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-K5IbmS/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i.pp.i:10198: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-K5IbmS/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i.pp.i:5166: 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.
KLEE: ERROR: /tmp/symbiotic-K5IbmS/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i.pp.i:5347: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-K5IbmS/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i.pp.i:10051: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-K5IbmS/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i.pp.i:10164: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-K5IbmS/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i.pp.i:5355: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-K5IbmS/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i.pp.i:5141: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-K5IbmS/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i.pp.i:9909: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-K5IbmS/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i.pp.i:10323: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-K5IbmS/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i.pp.i:10324: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-K5IbmS/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i.pp.i:5488: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-K5IbmS/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i.pp.i:9796: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-K5IbmS/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i.pp.i:10068: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-K5IbmS/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i.pp.i:5451: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-K5IbmS/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i.pp.i:10199: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-K5IbmS/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i.pp.i:10327: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-K5IbmS/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i.pp.i:9811: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
