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--scsi--megaraid--megaraid_mm.ko-entry_point_false-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.: 56 68 565 3321
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.24911403656
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to 'dma_pool_free' (function is undefined)
Removed calls to 'dma_pool_destroy' (function is undefined)
Defining function dma_pool_create as symbolic
Defining function printk as symbolic
Removed calls to '__list_del_entry' (function is undefined)
Defining function noop_llseek as symbolic
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function capable as symbolic
Removed calls to 'down' (function is undefined)
Removed calls to 'up' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'add_timer' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to '__might_fault' (function is undefined)
Removed calls to '__copy_from_user_overflow' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Removed calls to '__copy_to_user_overflow' (function is undefined)
Defining function _copy_to_user as symbolic
Defining function prepare_to_wait_event as symbolic
Defining function del_timer_sync as symbolic
Defining function _copy_from_user as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'ldv_check_final_state' (function is undefined)
Defining function ldv_release_2 as symbolic
Defining function misc_register as symbolic
Defining function misc_deregister as symbolic
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  memcmp
  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.327865123749
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 115 69 298 3051
INFO: Starting verification
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_9a22011b-f4c9-402b-a3b3-9f8e7c47cbf8/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-dVGbgU/linux-4.2-rc1.tar.xz-43_2a-drivers--scsi--megaraid--megaraid_mm.ko-entry_point_false-unreach-call.cil.out.c:5097: 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: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 14401 states (over memory cap)
KLEE: WARNING: killing 13799 states (over memory cap)
KLEE: WARNING: killing 14027 states (over memory cap)
KLEE: WARNING: killing 13436 states (over memory cap)
KLEE: WARNING: killing 13573 states (over memory cap)
KLEE: WARNING: killing 13817 states (over memory cap)
KLEE: WARNING: killing 13751 states (over memory cap)
KLEE: WARNING: killing 13493 states (over memory cap)
KLEE: WARNING: killing 13430 states (over memory cap)
KLEE: WARNING: killing 13567 states (over memory cap)
KLEE: WARNING: killing 14008 states (over memory cap)
KLEE: WARNING: killing 13457 states (over memory cap)
KLEE: WARNING: killing 13499 states (over memory cap)
KLEE: WARNING: killing 13937 states (over memory cap)
KLEE: WARNING: killing 13972 states (over memory cap)
KLEE: WARNING: killing 9789 states (over memory cap)
KLEE: WARNING: killing 13416 states (over memory cap)
KLEE: WARNING: killing 13558 states (over memory cap)
KLEE: WARNING: killing 9791 states (over memory cap)
KLEE: WARNING: killing 13378 states (over memory cap)
KLEE: WARNING: killing 9638 states (over memory cap)
KLEE: WARNING: killing 13777 states (over memory cap)
KLEE: WARNING: killing 13545 states (over memory cap)
KLEE: WARNING: killing 13583 states (over memory cap)
KLEE: WARNING: killing 9422 states (over memory cap)
KLEE: WARNING: killing 13602 states (over memory cap)
KLEE: WARNING: killing 13456 states (over memory cap)
KLEE: WARNING: killing 13411 states (over memory cap)
KLEE: WARNING: killing 9487 states (over memory cap)
KLEE: WARNING: killing 13245 states (over memory cap)
KLEE: WARNING: killing 9340 states (over memory cap)
KLEE: WARNING: killing 13086 states (over memory cap)
KLEE: WARNING: killing 9473 states (over memory cap)
KLEE: WARNING: killing 9363 states (over memory cap)
KLEE: WARNING: killing 13085 states (over memory cap)
KLEE: WARNING: killing 9959 states (over memory cap)
KLEE: WARNING: killing 13021 states (over memory cap)
KLEE: WARNING: killing 9629 states (over memory cap)
KLEE: WARNING: killing 13034 states (over memory cap)
KLEE: WARNING: killing 9400 states (over memory cap)
KLEE: WARNING: killing 9021 states (over memory cap)
KLEE: WARNING: killing 9185 states (over memory cap)
KLEE: WARNING: killing 9076 states (over memory cap)
KLEE: WARNING: killing 12808 states (over memory cap)
KLEE: WARNING: killing 9478 states (over memory cap)
KLEE: WARNING: killing 9010 states (over memory cap)
KLEE: WARNING: killing 9174 states (over memory cap)
KLEE: WARNING: killing 8984 states (over memory cap)
KLEE: WARNING: killing 8879 states (over memory cap)
KLEE: WARNING: killing 9126 states (over memory cap)
KLEE: WARNING: killing 12897 states (over memory cap)
KLEE: WARNING: killing 9515 states (over memory cap)
KLEE: WARNING: killing 8887 states (over memory cap)
KLEE: WARNING: killing 9134 states (over memory cap)
KLEE: WARNING: killing 9285 states (over memory cap)
KLEE: WARNING: killing 9010 states (over memory cap)
KLEE: WARNING: killing 8816 states (over memory cap)
KLEE: WARNING: killing 8979 states (over memory cap)
KLEE: WARNING: killing 9138 states (over memory cap)
KLEE: WARNING: killing 9205 states (over memory cap)
KLEE: WARNING: killing 8844 states (over memory cap)
KLEE: WARNING: killing 9349 states (over memory cap)
KLEE: WARNING: killing 9419 states (over memory cap)
KLEE: WARNING: killing 8717 states (over memory cap)
KLEE: WARNING: killing 8785 states (over memory cap)
KLEE: WARNING: killing 9116 states (over memory cap)
KLEE: WARNING: killing 8931 states (over memory cap)
KLEE: WARNING: killing 9169 states (over memory cap)
