bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--atm--solos-pci.ko-entry_point_true-unreach-call.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.: 440 150 1983 11784
Removed infinite loop in dma_unmap_single_attrs
Removed infinite loop in dma_map_single_attrs
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.67947101593
Removed calls to 'dev_warn' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to 'skb_unlink' (function is undefined)
Removed calls to '__dev_kfree_skb_any' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to 'consume_skb' (function is undefined)
Defining function skb_push as symbolic
Removed calls to 'skb_queue_tail' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'iowrite32' (function is undefined)
Removed calls to '__dev_kfree_skb_irq' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Defining function ioread32 as symbolic
Removed calls to 'debug_dma_unmap_page' (function is undefined)
Defining function skb_dequeue as symbolic
Removed calls to 'debug_dma_map_page' (function is undefined)
Defining function skb_pull as symbolic
Defining function sprintf as symbolic
Defining function strcat as symbolic
Defining function printk as symbolic
Defining function __phys_addr as symbolic
Defining function skb_put as symbolic
Defining function prepare_to_wait_event as symbolic
Defining function schedule_timeout as symbolic
Defining function net_ratelimit as symbolic
Removed calls to 'kfree_skb' (function is undefined)
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Defining function snprintf as symbolic
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to '_dev_info' (function is undefined)
Removed calls to 'pci_set_master' (function is undefined)
Removed calls to 'tasklet_init' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'dev_err' (function is undefined)
Removed calls to 'atm_dev_signal_change' (function is undefined)
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'tasklet_kill' (function is undefined)
Removed calls to 'pci_iounmap' (function is undefined)
Removed calls to 'pci_release_regions' (function is undefined)
Removed calls to 'sysfs_remove_group' (function is undefined)
Removed calls to 'pci_disable_device' (function is undefined)
Removed calls to 'atm_dev_deregister' (function is undefined)
Defining function pci_enable_device as symbolic
Defining function pci_request_regions as symbolic
Defining function pci_iomap as symbolic
Removed calls to '_raw_read_lock' (function is undefined)
Removed calls to '_raw_read_unlock' (function is undefined)
Defining function sysfs_create_group as symbolic
Defining function device_create_file as symbolic
Defining function atm_dev_register as symbolic
Defining function request_threaded_irq as symbolic
Removed calls to '__tasklet_schedule' (function is undefined)
Defining function atm_charge as symbolic
Defining function simple_strtol as symbolic
Defining function dma_set_mask as symbolic
Defining function dma_supported as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'pci_unregister_driver' (function is undefined)
Removed calls to 'ldv_check_final_state' (function is undefined)
Defining function ldv_shutdown_2 as symbolic
Defining function __pci_register_driver as symbolic
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  strcmp
  strlen
  strncmp
  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.717386960983
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 532 125 922 7363
INFO: Starting verification
KLEE: WARNING ONCE: function "popen" has inline asm
KLEE: WARNING ONCE: function "pclose" has inline asm
KLEE: WARNING ONCE: function "fpga_tx" has inline asm
KLEE: WARNING ONCE: function "dma_unmap_single_attrs" has inline asm
KLEE: WARNING ONCE: function "dma_map_single_attrs" has inline asm
KLEE: WARNING ONCE: function "solos_param_show" has inline asm
KLEE: WARNING ONCE: function "solos_param_store" has inline asm
KLEE: WARNING ONCE: function "tasklet_schedule" 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_b89b9495-82a8-481f-aaec-3dde9053b154/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 81106 states (over memory cap)
KLEE: WARNING: killing 47807 states (over memory cap)
KLEE: WARNING: killing 71174 states (over memory cap)
KLEE: WARNING: killing 55231 states (over memory cap)
KLEE: WARNING: killing 71455 states (over memory cap)
KLEE: WARNING: killing 67273 states (over memory cap)
KLEE: WARNING: killing 79070 states (over memory cap)
KLEE: WARNING: killing 68878 states (over memory cap)
KLEE: WARNING: killing 71178 states (over memory cap)
KLEE: WARNING: killing 58707 states (over memory cap)
KLEE: WARNING: killing 73915 states (over memory cap)
KLEE: WARNING: killing 68619 states (over memory cap)
KLEE: WARNING: killing 67351 states (over memory cap)
KLEE: WARNING: killing 67860 states (over memory cap)
KLEE: WARNING: killing 72331 states (over memory cap)
KLEE: WARNING: killing 68749 states (over memory cap)
KLEE: WARNING: killing 67586 states (over memory cap)
KLEE: WARNING: killing 70495 states (over memory cap)
KLEE: WARNING: killing 67491 states (over memory cap)
KLEE: WARNING: killing 71030 states (over memory cap)
KLEE: WARNING: killing 63648 states (over memory cap)
KLEE: WARNING: killing 75998 states (over memory cap)
KLEE: WARNING: killing 64526 states (over memory cap)
KLEE: WARNING: killing 75351 states (over memory cap)
KLEE: WARNING: killing 67096 states (over memory cap)
KLEE: WARNING: killing 68731 states (over memory cap)
KLEE: WARNING: killing 70970 states (over memory cap)
KLEE: WARNING: killing 65171 states (over memory cap)
KLEE: WARNING: killing 71523 states (over memory cap)
KLEE: WARNING: killing 69100 states (over memory cap)
KLEE: WARNING: killing 70736 states (over memory cap)
KLEE: WARNING: killing 72490 states (over memory cap)
KLEE: WARNING: killing 70892 states (over memory cap)
KLEE: WARNING: killing 65245 states (over memory cap)
KLEE: WARNING: killing 70941 states (over memory cap)
KLEE: WARNING: killing 62382 states (over memory cap)
KLEE: WARNING: killing 75086 states (over memory cap)
KLEE: WARNING: killing 66809 states (over memory cap)
KLEE: WARNING: killing 78801 states (over memory cap)
KLEE: WARNING: killing 59966 states (over memory cap)
KLEE: WARNING: killing 79493 states (over memory cap)
KLEE: WARNING: killing 61762 states (over memory cap)
KLEE: WARNING: killing 77376 states (over memory cap)
KLEE: WARNING: killing 69219 states (over memory cap)
KLEE: WARNING: killing 65265 states (over memory cap)
KLEE: WARNING: killing 74699 states (over memory cap)
