bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_bitvector_linux-3.16-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.: 54 65 561 3322
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.226101875305
Defining function printk as symbolic
Defining function dma_pool_alloc as symbolic
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to 'dma_pool_free' (function is undefined)
Removed calls to 'dma_pool_destroy' (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 '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 '__list_add' (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 kmem_cache_alloc as symbolic
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  memcmp
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_assume
  __VERIFIER_calloc0
  __VERIFIER_error
  __VERIFIER_exit
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
  __VERIFIER_nondet_loff_t_named
  __VERIFIER_nondet_pointer_named
  __VERIFIER_nondet_uint_named
  __VERIFIER_nondet_ulong_named
INFO: After-slicing optimizations and preparation time: 0.276726007462
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 116 68 277 2730
INFO: Starting verification
KLEE: ERROR: /tmp/symbiotic-e04Yea/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--scsi--megaraid--megaraid_mm.ko-entry_point_false-unreach-call.cil.out.c:5126: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_ebcea766-2a66-4da3-a1af-aece744b9271/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
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 11941 states (over memory cap)
KLEE: WARNING: killing 9193 states (over memory cap)
KLEE: WARNING: killing 9158 states (over memory cap)
KLEE: WARNING: killing 9299 states (over memory cap)
KLEE: WARNING: killing 9440 states (over memory cap)
KLEE: WARNING: killing 9495 states (over memory cap)
KLEE: WARNING: killing 9380 states (over memory cap)
KLEE: WARNING: killing 9433 states (over memory cap)
KLEE: WARNING: killing 9406 states (over memory cap)
KLEE: WARNING: killing 9201 states (over memory cap)
KLEE: WARNING: killing 9087 states (over memory cap)
KLEE: WARNING: killing 9406 states (over memory cap)
KLEE: WARNING: killing 9555 states (over memory cap)
KLEE: WARNING: killing 9098 states (over memory cap)
KLEE: WARNING: killing 9589 states (over memory cap)
KLEE: WARNING: killing 9477 states (over memory cap)
KLEE: WARNING: killing 9191 states (over memory cap)
KLEE: WARNING: killing 9169 states (over memory cap)
KLEE: WARNING: killing 9399 states (over memory cap)
KLEE: WARNING: killing 9545 states (over memory cap)
KLEE: WARNING: killing 9523 states (over memory cap)
KLEE: WARNING: killing 9586 states (over memory cap)
KLEE: WARNING: killing 9475 states (over memory cap)
KLEE: WARNING: killing 9706 states (over memory cap)
KLEE: WARNING: killing 9515 states (over memory cap)
KLEE: WARNING: killing 9323 states (over memory cap)
KLEE: WARNING: killing 9719 states (over memory cap)
KLEE: WARNING: killing 9861 states (over memory cap)
KLEE: WARNING: killing 9758 states (over memory cap)
KLEE: WARNING: killing 9402 states (over memory cap)
KLEE: WARNING: killing 9623 states (over memory cap)
KLEE: WARNING: killing 9524 states (over memory cap)
KLEE: WARNING: killing 9421 states (over memory cap)
KLEE: WARNING: killing 9887 states (over memory cap)
KLEE: WARNING: killing 9372 states (over memory cap)
KLEE: WARNING: killing 9592 states (over memory cap)
KLEE: WARNING: killing 9740 states (over memory cap)
KLEE: WARNING: killing 9220 states (over memory cap)
KLEE: WARNING: killing 9357 states (over memory cap)
KLEE: WARNING: killing 9586 states (over memory cap)
KLEE: WARNING: killing 9403 states (over memory cap)
KLEE: WARNING: killing 9296 states (over memory cap)
KLEE: WARNING: killing 9681 states (over memory cap)
KLEE: WARNING: killing 9503 states (over memory cap)
KLEE: WARNING: killing 9404 states (over memory cap)
KLEE: WARNING: killing 9543 states (over memory cap)
KLEE: WARNING: killing 9523 states (over memory cap)
KLEE: WARNING: killing 9340 states (over memory cap)
KLEE: WARNING: killing 9404 states (over memory cap)
KLEE: WARNING: killing 9541 states (over memory cap)
KLEE: WARNING: killing 9518 states (over memory cap)
KLEE: WARNING: killing 9659 states (over memory cap)
KLEE: WARNING: killing 9563 states (over memory cap)
KLEE: WARNING: killing 9461 states (over memory cap)
KLEE: WARNING: killing 9524 states (over memory cap)
KLEE: WARNING: killing 9899 states (over memory cap)
KLEE: WARNING: killing 9410 states (over memory cap)
KLEE: WARNING: killing 9387 states (over memory cap)
KLEE: WARNING: killing 9138 states (over memory cap)
KLEE: WARNING: killing 9352 states (over memory cap)
KLEE: WARNING: killing 9497 states (over memory cap)
KLEE: WARNING: killing 9400 states (over memory cap)
KLEE: WARNING: killing 9698 states (over memory cap)
KLEE: WARNING: killing 9833 states (over memory cap)
KLEE: WARNING: killing 9351 states (over memory cap)
KLEE: WARNING: killing 9491 states (over memory cap)
KLEE: WARNING: killing 9389 states (over memory cap)
KLEE: WARNING: killing 9452 states (over memory cap)
KLEE: WARNING: killing 9203 states (over memory cap)
KLEE: WARNING: killing 9569 states (over memory cap)
KLEE: WARNING: killing 9398 states (over memory cap)
KLEE: WARNING: killing 9378 states (over memory cap)
KLEE: WARNING: killing 9436 states (over memory cap)
KLEE: WARNING: killing 9720 states (over memory cap)
KLEE: WARNING: killing 9248 states (over memory cap)
KLEE: WARNING: killing 9384 states (over memory cap)
KLEE: WARNING: killing 9372 states (over memory cap)
KLEE: WARNING: killing 9810 states (over memory cap)
KLEE: WARNING: killing 9491 states (over memory cap)
KLEE: WARNING: killing 9706 states (over memory cap)
KLEE: WARNING: killing 9616 states (over memory cap)
KLEE: WARNING: killing 9597 states (over memory cap)
KLEE: WARNING: killing 9208 states (over memory cap)
