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-08_1a-drivers--rapidio--rapidio.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.: 280 208 1465 10506
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 0.442743062973
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function device_add as symbolic
Defining function device_create_bin_file as symbolic
Defining function device_create_file as symbolic
Defining function printk as symbolic
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Removed calls to '__dynamic_pr_debug' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Defining function __dma_request_channel as symbolic
Removed calls to 'dma_release_channel' (function is undefined)
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to 'dev_err' (function is undefined)
Removed calls to '__dynamic_dev_dbg' (function is undefined)
Defining function dev_set_name as symbolic
Defining function device_register as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'put_device' (function is undefined)
Defining function get_device as symbolic
Defining function request_resource as symbolic
Defining function release_resource as symbolic
Removed calls to 'destroy_workqueue' (function is undefined)
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to 'flush_workqueue' (function is undefined)
Defining function __alloc_workqueue_key as symbolic
Defining function queue_work_on as symbolic
Defining function add_uevent_var as symbolic
Defining function driver_register as symbolic
Removed calls to 'driver_unregister' (function is undefined)
Defining function sprintf as symbolic
Defining function capable as symbolic
Defining function kstrtoll as symbolic
Defining function queue_delayed_work_on as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'ldv_module_exit' (function is undefined)
Removed calls to 'class_unregister' (function is undefined)
Defining function ldv_release_5 as symbolic
Defining function ldv_probe_5 as symbolic
Defining function __class_register as symbolic
Defining function bus_register as symbolic
Removed calls to 'device_remove_bin_file' (function is undefined)
Removed calls to 'device_remove_file' (function is undefined)
Linked our definitions to these undefined functions:
  __kmalloc
  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.512326955795
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 355 198 939 6792
INFO: Starting verification
KLEE: WARNING ONCE: function "rio_request_mport_dma" has inline asm
KLEE: WARNING ONCE: function "rio_request_dma" has inline asm
KLEE: WARNING ONCE: function "rio_get_asm" 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_854745d7-9f8d-449a-a45a-92b8ae931955/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 31718 states (over memory cap)
KLEE: WARNING: killing 25988 states (over memory cap)
KLEE: WARNING: killing 24080 states (over memory cap)
KLEE: WARNING: killing 24008 states (over memory cap)
KLEE: WARNING: killing 22357 states (over memory cap)
KLEE: WARNING: killing 21575 states (over memory cap)
KLEE: WARNING: killing 22238 states (over memory cap)
KLEE: WARNING: killing 21702 states (over memory cap)
KLEE: WARNING: killing 21521 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-8nlWQ3/linux-4.2-rc1.tar.xz-08_1a-drivers--rapidio--rapidio.ko-entry_point_true-unreach-call.cil.out.c:6851: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 21236 states (over memory cap)
KLEE: WARNING: killing 22744 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-8nlWQ3/linux-4.2-rc1.tar.xz-08_1a-drivers--rapidio--rapidio.ko-entry_point_true-unreach-call.cil.out.c:6715: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 23529 states (over memory cap)
KLEE: WARNING: killing 24199 states (over memory cap)
KLEE: WARNING: killing 23671 states (over memory cap)
KLEE: WARNING: killing 23272 states (over memory cap)
KLEE: WARNING: killing 24175 states (over memory cap)
KLEE: WARNING: killing 23895 states (over memory cap)
KLEE: WARNING: killing 25627 states (over memory cap)
KLEE: WARNING: killing 24876 states (over memory cap)
KLEE: WARNING: killing 26024 states (over memory cap)
KLEE: WARNING: killing 26929 states (over memory cap)
KLEE: WARNING: killing 26315 states (over memory cap)
KLEE: WARNING: killing 26271 states (over memory cap)
KLEE: WARNING: killing 25191 states (over memory cap)
KLEE: WARNING: killing 25633 states (over memory cap)
KLEE: WARNING: killing 26428 states (over memory cap)
KLEE: WARNING: killing 26855 states (over memory cap)
KLEE: WARNING: killing 27181 states (over memory cap)
KLEE: WARNING: killing 27272 states (over memory cap)
KLEE: WARNING: killing 25717 states (over memory cap)
KLEE: WARNING: killing 26275 states (over memory cap)
KLEE: WARNING: killing 25077 states (over memory cap)
KLEE: WARNING: killing 24110 states (over memory cap)
KLEE: WARNING: killing 23377 states (over memory cap)
KLEE: WARNING: killing 24149 states (over memory cap)
KLEE: WARNING: killing 24694 states (over memory cap)
KLEE: WARNING: killing 24778 states (over memory cap)
KLEE: WARNING: killing 25552 states (over memory cap)
KLEE: WARNING: killing 24837 states (over memory cap)
KLEE: WARNING: killing 24339 states (over memory cap)
KLEE: WARNING: killing 25690 states (over memory cap)
KLEE: WARNING: killing 24854 states (over memory cap)
KLEE: WARNING: killing 25177 states (over memory cap)
KLEE: WARNING: killing 23538 states (over memory cap)
KLEE: WARNING: killing 24991 states (over memory cap)
KLEE: WARNING: killing 25080 states (over memory cap)
KLEE: WARNING: killing 25276 states (over memory cap)
KLEE: WARNING: killing 26506 states (over memory cap)
KLEE: WARNING: killing 24769 states (over memory cap)
KLEE: WARNING: killing 23945 states (over memory cap)
KLEE: WARNING: killing 24475 states (over memory cap)
KLEE: WARNING: killing 25811 states (over memory cap)
KLEE: WARNING: killing 25218 states (over memory cap)
KLEE: WARNING: killing 24969 states (over memory cap)
KLEE: WARNING: killing 23909 states (over memory cap)
KLEE: WARNING: killing 25466 states (over memory cap)
KLEE: WARNING: killing 25553 states (over memory cap)
KLEE: WARNING: killing 24947 states (over memory cap)
KLEE: WARNING: killing 24695 states (over memory cap)
KLEE: WARNING: killing 25913 states (over memory cap)
KLEE: WARNING: killing 25314 states (over memory cap)
KLEE: WARNING: killing 25846 states (over memory cap)
KLEE: WARNING: killing 25369 states (over memory cap)
KLEE: WARNING: killing 25447 states (over memory cap)
KLEE: WARNING: killing 24965 states (over memory cap)
KLEE: WARNING: killing 25511 states (over memory cap)
KLEE: WARNING: killing 24806 states (over memory cap)
KLEE: WARNING: killing 24447 states (over memory cap)
KLEE: WARNING: killing 25195 states (over memory cap)
KLEE: WARNING: killing 24939 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-8nlWQ3/linux-4.2-rc1.tar.xz-08_1a-drivers--rapidio--rapidio.ko-entry_point_true-unreach-call.cil.out.c:7664: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 24580 states (over memory cap)
KLEE: WARNING: killing 25220 states (over memory cap)
KLEE: WARNING: killing 24528 states (over memory cap)
KLEE: WARNING: killing 23943 states (over memory cap)
KLEE: WARNING: killing 24581 states (over memory cap)
KLEE: WARNING: killing 25438 states (over memory cap)
KLEE: WARNING: killing 24403 states (over memory cap)
KLEE: WARNING: killing 24822 states (over memory cap)
KLEE: WARNING: killing 26003 states (over memory cap)
KLEE: WARNING: killing 25976 states (over memory cap)
KLEE: WARNING: killing 25289 states (over memory cap)
KLEE: WARNING: killing 25484 states (over memory cap)
KLEE: WARNING: killing 24130 states (over memory cap)
KLEE: WARNING: killing 24758 states (over memory cap)
KLEE: WARNING: killing 24188 states (over memory cap)
KLEE: WARNING: killing 25037 states (over memory cap)
KLEE: WARNING: killing 24788 states (over memory cap)
KLEE: WARNING: killing 24654 states (over memory cap)
KLEE: WARNING: killing 25493 states (over memory cap)
KLEE: WARNING: killing 25805 states (over memory cap)
KLEE: WARNING: killing 25549 states (over memory cap)
KLEE: WARNING: killing 25409 states (over memory cap)
KLEE: WARNING: killing 24729 states (over memory cap)
KLEE: WARNING: killing 25793 states (over memory cap)
KLEE: WARNING: killing 25002 states (over memory cap)
KLEE: WARNING: killing 25622 states (over memory cap)
KLEE: WARNING: killing 25167 states (over memory cap)
KLEE: WARNING: killing 25248 states (over memory cap)
KLEE: WARNING: killing 25002 states (over memory cap)
KLEE: WARNING: killing 24536 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-8nlWQ3/linux-4.2-rc1.tar.xz-08_1a-drivers--rapidio--rapidio.ko-entry_point_true-unreach-call.cil.out.c:7993: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 24508 states (over memory cap)
KLEE: WARNING: killing 25122 states (over memory cap)
KLEE: WARNING: killing 24884 states (over memory cap)
KLEE: WARNING: killing 25395 states (over memory cap)
KLEE: WARNING: killing 25796 states (over memory cap)
KLEE: WARNING: killing 25235 states (over memory cap)
KLEE: WARNING: killing 24028 states (over memory cap)
KLEE: WARNING: killing 24543 states (over memory cap)
KLEE: WARNING: killing 25047 states (over memory cap)
KLEE: WARNING: killing 24906 states (over memory cap)
KLEE: WARNING: killing 25412 states (over memory cap)
KLEE: WARNING: killing 25717 states (over memory cap)
KLEE: WARNING: killing 25268 states (over memory cap)
KLEE: WARNING: killing 24812 states (over memory cap)
KLEE: WARNING: killing 26493 states (over memory cap)
KLEE: WARNING: killing 25087 states (over memory cap)
KLEE: WARNING: killing 26230 states (over memory cap)
KLEE: WARNING: killing 26529 states (over memory cap)
KLEE: WARNING: killing 25019 states (over memory cap)
KLEE: WARNING: killing 24895 states (over memory cap)
KLEE: WARNING: killing 24965 states (over memory cap)
KLEE: WARNING: killing 24627 states (over memory cap)
KLEE: WARNING: killing 23759 states (over memory cap)
KLEE: WARNING: killing 24157 states (over memory cap)
KLEE: WARNING: killing 25279 states (over memory cap)
KLEE: WARNING: killing 24943 states (over memory cap)
KLEE: WARNING: killing 25225 states (over memory cap)
KLEE: WARNING: killing 24357 states (over memory cap)
KLEE: WARNING: killing 25268 states (over memory cap)
KLEE: WARNING: killing 24821 states (over memory cap)
KLEE: WARNING: killing 25738 states (over memory cap)
KLEE: WARNING: killing 25300 states (over memory cap)
KLEE: WARNING: killing 24226 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-8nlWQ3/linux-4.2-rc1.tar.xz-08_1a-drivers--rapidio--rapidio.ko-entry_point_true-unreach-call.cil.out.c:7703: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 25354 states (over memory cap)
KLEE: WARNING: killing 25853 states (over memory cap)
KLEE: WARNING: killing 25309 states (over memory cap)
KLEE: WARNING: killing 24872 states (over memory cap)
KLEE: WARNING: killing 24114 states (over memory cap)
KLEE: WARNING: killing 25022 states (over memory cap)
KLEE: WARNING: killing 25199 states (over memory cap)
KLEE: WARNING: killing 24976 states (over memory cap)
KLEE: WARNING: killing 25570 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-8nlWQ3/linux-4.2-rc1.tar.xz-08_1a-drivers--rapidio--rapidio.ko-entry_point_true-unreach-call.cil.out.c:7533: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 25548 states (over memory cap)
KLEE: WARNING: killing 24603 states (over memory cap)
KLEE: WARNING: killing 25910 states (over memory cap)
KLEE: WARNING: killing 24334 states (over memory cap)
KLEE: WARNING: killing 24721 states (over memory cap)
KLEE: WARNING: killing 23877 states (over memory cap)
KLEE: WARNING: killing 24569 states (over memory cap)
KLEE: WARNING: killing 25590 states (over memory cap)
KLEE: WARNING: killing 24938 states (over memory cap)
KLEE: WARNING: killing 24096 states (over memory cap)
KLEE: WARNING: killing 25303 states (over memory cap)
KLEE: WARNING: killing 25693 states (over memory cap)
KLEE: WARNING: killing 25672 states (over memory cap)
KLEE: WARNING: killing 25642 states (over memory cap)
KLEE: WARNING: killing 24811 states (over memory cap)
KLEE: WARNING: killing 25192 states (over memory cap)
KLEE: WARNING: killing 25984 states (over memory cap)
KLEE: WARNING: killing 25052 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-8nlWQ3/linux-4.2-rc1.tar.xz-08_1a-drivers--rapidio--rapidio.ko-entry_point_true-unreach-call.cil.out.c:7501: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 25428 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-8nlWQ3/linux-4.2-rc1.tar.xz-08_1a-drivers--rapidio--rapidio.ko-entry_point_true-unreach-call.cil.out.c:7614: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8nlWQ3/linux-4.2-rc1.tar.xz-08_1a-drivers--rapidio--rapidio.ko-entry_point_true-unreach-call.cil.out.c:7582: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 25616 states (over memory cap)
KLEE: WARNING: killing 23873 states (over memory cap)
KLEE: WARNING: killing 25363 states (over memory cap)
KLEE: WARNING: killing 23919 states (over memory cap)
