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--md--dm-snapshot.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.: 157 241 2027 12474
Removed infinite loop in snapshot_dtr
Removed infinite loop in snapshot_merge_next_chunks
Removed infinite loop in dm_consecutive_chunk_count_dec
Removed infinite loop in dm_consecutive_chunk_count_inc
Removed infinite loop in persistent_commit_merge
Removed infinite loop in get_exception
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.470696926117
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)
Removed calls to 'list_del' (function is undefined)
Removed calls to 'module_put' (function is undefined)
Defining function kstrtouint as symbolic
Defining function kstrdup as symbolic
Defining function printk as symbolic
Defining function __request_module as symbolic
Defining function try_module_get as symbolic
Removed calls to '__init_rwsem' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'down_write' (function is undefined)
Removed calls to 'up_write' (function is undefined)
Removed calls to 'mempool_destroy' (function is undefined)
Removed calls to 'dm_kcopyd_client_destroy' (function is undefined)
Removed calls to 'dm_put_device' (function is undefined)
Removed calls to 'down_read' (function is undefined)
Removed calls to 'up_read' (function is undefined)
Removed calls to 'msleep' (function is undefined)
Removed calls to 'mempool_free' (function is undefined)
Removed calls to 'generic_make_request' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'dm_internal_suspend_fast' (function is undefined)
Removed calls to 'down_write_nested' (function is undefined)
Removed calls to 'dm_internal_resume_fast' (function is undefined)
Removed calls to 'dm_put' (function is undefined)
Defining function scnprintf as symbolic
Defining function dm_table_get_md as symbolic
Defining function dm_hold as symbolic
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 'wake_up_bit' (function is undefined)
Defining function prepare_to_wait_event as symbolic
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Removed calls to 'kmem_cache_free' (function is undefined)
Removed calls to 'bio_endio' (function is undefined)
Defining function dm_kcopyd_copy as symbolic
Defining function dm_table_get_size as symbolic
Removed calls to 'dm_table_event' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Defining function bit_wait as symbolic
Defining function out_of_line_wait_on_bit as symbolic
Defining function dm_suspended as symbolic
Defining function dm_kcopyd_prepare_callback as symbolic
Removed calls to 'dm_kcopyd_do_callback' (function is undefined)
Removed calls to 'vfree' (function is undefined)
Defining function dm_get_device as symbolic
Defining function dm_table_get_mode as symbolic
Defining function dm_kcopyd_client_create as symbolic
Defining function dm_set_target_max_io_len as symbolic
Defining function mempool_alloc_slab as symbolic
Defining function mempool_create as symbolic
Defining function dm_vcalloc as symbolic
Removed calls to 'dm_accept_partial_bio' (function is undefined)
Defining function snprintf as symbolic
Removed calls to 'destroy_workqueue' (function is undefined)
Removed calls to 'dm_io_client_destroy' (function is undefined)
Removed calls to 'dm_bufio_set_minimum_buffers' (function is undefined)
Removed calls to 'dm_bufio_prefetch' (function is undefined)
Removed calls to 'dm_bufio_release' (function is undefined)
Removed calls to 'dm_bufio_forget' (function is undefined)
Removed calls to 'dm_bufio_client_destroy' (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)
Removed calls to 'destroy_work_on_stack' (function is undefined)
Defining function dm_io as symbolic
Defining function queue_work_on as symbolic
Defining function dm_bufio_client_create as symbolic
Defining function dm_bufio_get_device_size as symbolic
Defining function dm_bufio_read as symbolic
Defining function dm_io_client_create as symbolic
Defining function __alloc_workqueue_key as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'dm_unregister_target' (function is undefined)
Removed calls to 'kmem_cache_destroy' (function is undefined)
Removed calls to 'ldv_check_final_state' (function is undefined)
Defining function ldv_presuspend_6 as symbolic
Defining function ldv_postsuspend_6 as symbolic
Defining function ldv_presuspend_7 as symbolic
Defining function ldv_preresume_7 as symbolic
Defining function ldv_postsuspend_5 as symbolic
Defining function dm_register_target as symbolic
Defining function kmem_cache_create as symbolic
Defining function ldv_release_4 as symbolic
Defining function ldv_probe_4 as symbolic
Defining function ldv_release_1 as symbolic
Defining function ldv_probe_1 as symbolic
Defining function ldv_release_2 as symbolic
Defining function ldv_probe_2 as symbolic
Defining function ldv_release_3 as symbolic
Defining function ldv_probe_3 as symbolic
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  strcmp
  strrchr
  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.51811504364
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 262 183 1202 7824
INFO: Starting verification
KLEE: WARNING ONCE: function "dm_exception_store_set_chunk_size" has inline asm
KLEE: WARNING ONCE: function "snapshot_ctr" has inline asm
KLEE: WARNING ONCE: function "snapshot_dtr" has inline asm
KLEE: WARNING ONCE: function "snapshot_map" has inline asm
KLEE: WARNING ONCE: function "stop_merge" has inline asm
KLEE: WARNING ONCE: function "start_merge" has inline asm
KLEE: WARNING ONCE: function "snapshot_merge_next_chunks" has inline asm
KLEE: WARNING ONCE: function "__origin_write" has inline asm
KLEE: WARNING ONCE: function "merge_callback" has inline asm
KLEE: WARNING ONCE: function "__find_pending_exception" has inline asm
KLEE: WARNING ONCE: function "pending_complete" has inline asm
KLEE: WARNING ONCE: function "dm_consecutive_chunk_count_inc" has inline asm
KLEE: WARNING ONCE: function "persistent_read_metadata" has inline asm
KLEE: WARNING ONCE: function "persistent_prepare_exception" has inline asm
KLEE: WARNING ONCE: function "persistent_commit_exception" has inline asm
KLEE: WARNING ONCE: function "persistent_prepare_merge" has inline asm
KLEE: WARNING ONCE: function "persistent_commit_merge" has inline asm
KLEE: WARNING: undefined reference to function: mempool_free_slab
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_46326722-f231-45c8-819c-e77ccd545da1/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Hr64DD/linux-4.2-rc1.tar.xz-43_2a-drivers--md--dm-snapshot.ko-entry_point_true-unreach-call.cil.out.c:8724: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 17002 states (over memory cap)
KLEE: WARNING: killing 12882 states (over memory cap)
KLEE: WARNING: killing 12403 states (over memory cap)
KLEE: WARNING: killing 11806 states (over memory cap)
KLEE: WARNING: killing 12220 states (over memory cap)
KLEE: WARNING: killing 12317 states (over memory cap)
KLEE: WARNING: killing 12795 states (over memory cap)
KLEE: WARNING: killing 12139 states (over memory cap)
KLEE: WARNING: killing 12054 states (over memory cap)
KLEE: WARNING: killing 12410 states (over memory cap)
KLEE: WARNING: killing 12571 states (over memory cap)
KLEE: WARNING: killing 13116 states (over memory cap)
KLEE: WARNING: killing 13283 states (over memory cap)
KLEE: WARNING: killing 13640 states (over memory cap)
KLEE: WARNING: killing 13619 states (over memory cap)
KLEE: WARNING: killing 13600 states (over memory cap)
KLEE: WARNING: killing 13956 states (over memory cap)
KLEE: WARNING: killing 12950 states (over memory cap)
KLEE: WARNING: killing 13307 states (over memory cap)
KLEE: WARNING: killing 13037 states (over memory cap)
KLEE: WARNING: killing 13081 states (over memory cap)
KLEE: WARNING: killing 12692 states (over memory cap)
KLEE: WARNING: killing 12798 states (over memory cap)
KLEE: WARNING: killing 13148 states (over memory cap)
KLEE: WARNING: killing 12702 states (over memory cap)
KLEE: WARNING: killing 12994 states (over memory cap)
KLEE: WARNING: killing 12486 states (over memory cap)
KLEE: WARNING: killing 13076 states (over memory cap)
KLEE: WARNING: killing 12693 states (over memory cap)
KLEE: WARNING: killing 13043 states (over memory cap)
KLEE: WARNING: killing 13273 states (over memory cap)
KLEE: WARNING: killing 12651 states (over memory cap)
KLEE: WARNING: killing 12819 states (over memory cap)
KLEE: WARNING: killing 13044 states (over memory cap)
KLEE: WARNING: killing 12968 states (over memory cap)
KLEE: WARNING: killing 12770 states (over memory cap)
KLEE: WARNING: killing 12693 states (over memory cap)
KLEE: WARNING: killing 13043 states (over memory cap)
KLEE: WARNING: killing 13574 states (over memory cap)
KLEE: WARNING: killing 12534 states (over memory cap)
KLEE: WARNING: killing 13301 states (over memory cap)
KLEE: WARNING: killing 12925 states (over memory cap)
KLEE: WARNING: killing 13331 states (over memory cap)
KLEE: WARNING: killing 12659 states (over memory cap)
KLEE: WARNING: killing 13363 states (over memory cap)
KLEE: WARNING: killing 13289 states (over memory cap)
KLEE: WARNING: killing 12917 states (over memory cap)
KLEE: WARNING: killing 12544 states (over memory cap)
KLEE: WARNING: killing 12824 states (over memory cap)
KLEE: WARNING: killing 12810 states (over memory cap)
KLEE: WARNING: killing 12859 states (over memory cap)
KLEE: WARNING: killing 12663 states (over memory cap)
KLEE: WARNING: killing 12356 states (over memory cap)
KLEE: WARNING: killing 12878 states (over memory cap)
KLEE: WARNING: killing 13278 states (over memory cap)
KLEE: WARNING: killing 12732 states (over memory cap)
KLEE: WARNING: killing 13075 states (over memory cap)
KLEE: WARNING: killing 12949 states (over memory cap)
KLEE: WARNING: killing 12873 states (over memory cap)
KLEE: WARNING: killing 12445 states (over memory cap)
KLEE: WARNING: killing 12786 states (over memory cap)
KLEE: WARNING: killing 12949 states (over memory cap)
KLEE: WARNING: killing 13174 states (over memory cap)
KLEE: WARNING: killing 13219 states (over memory cap)
KLEE: WARNING: killing 12737 states (over memory cap)
KLEE: WARNING: killing 13373 states (over memory cap)
KLEE: WARNING: killing 12719 states (over memory cap)
KLEE: WARNING: killing 12172 states (over memory cap)
KLEE: WARNING: killing 12978 states (over memory cap)
KLEE: WARNING: killing 12967 states (over memory cap)
KLEE: WARNING: killing 13072 states (over memory cap)
KLEE: WARNING: killing 13062 states (over memory cap)
KLEE: WARNING: killing 12757 states (over memory cap)
KLEE: WARNING: killing 13095 states (over memory cap)
KLEE: WARNING: killing 13142 states (over memory cap)
KLEE: WARNING: killing 12894 states (over memory cap)
KLEE: WARNING: killing 12883 states (over memory cap)
KLEE: WARNING: killing 12641 states (over memory cap)
KLEE: WARNING: killing 13211 states (over memory cap)
KLEE: WARNING: killing 13077 states (over memory cap)
KLEE: WARNING: killing 12836 states (over memory cap)
KLEE: WARNING: killing 13110 states (over memory cap)
KLEE: WARNING: killing 12814 states (over memory cap)
KLEE: WARNING: killing 13030 states (over memory cap)
KLEE: WARNING: killing 12322 states (over memory cap)
KLEE: WARNING: killing 12951 states (over memory cap)
KLEE: WARNING: killing 12594 states (over memory cap)
KLEE: WARNING: killing 13331 states (over memory cap)
KLEE: WARNING: killing 12916 states (over memory cap)
KLEE: WARNING: killing 13135 states (over memory cap)
KLEE: WARNING: killing 12668 states (over memory cap)
KLEE: WARNING: killing 12767 states (over memory cap)
KLEE: WARNING: killing 13163 states (over memory cap)
KLEE: WARNING: killing 12918 states (over memory cap)
KLEE: WARNING: killing 12968 states (over memory cap)
KLEE: WARNING: killing 12780 states (over memory cap)
KLEE: WARNING: killing 13113 states (over memory cap)
KLEE: WARNING: killing 12645 states (over memory cap)
KLEE: WARNING: killing 12690 states (over memory cap)
KLEE: WARNING: killing 12448 states (over memory cap)
KLEE: WARNING: killing 13116 states (over memory cap)
KLEE: WARNING: killing 13049 states (over memory cap)
KLEE: WARNING: killing 13328 states (over memory cap)
KLEE: WARNING: killing 12917 states (over memory cap)
KLEE: WARNING: killing 12681 states (over memory cap)
KLEE: WARNING: killing 12784 states (over memory cap)
KLEE: WARNING: killing 12258 states (over memory cap)
KLEE: WARNING: killing 12875 states (over memory cap)
KLEE: WARNING: killing 13090 states (over memory cap)
KLEE: WARNING: killing 13023 states (over memory cap)
KLEE: WARNING: killing 12842 states (over memory cap)
KLEE: WARNING: killing 12723 states (over memory cap)
KLEE: WARNING: killing 12992 states (over memory cap)
KLEE: WARNING: killing 13211 states (over memory cap)
KLEE: WARNING: killing 12805 states (over memory cap)
KLEE: WARNING: killing 12741 states (over memory cap)
KLEE: WARNING: killing 12724 states (over memory cap)
KLEE: WARNING: killing 12994 states (over memory cap)
KLEE: WARNING: killing 12537 states (over memory cap)
KLEE: WARNING: killing 13368 states (over memory cap)
KLEE: WARNING: killing 12965 states (over memory cap)
KLEE: WARNING: killing 12840 states (over memory cap)
KLEE: WARNING: killing 12601 states (over memory cap)
KLEE: WARNING: killing 12930 states (over memory cap)
KLEE: WARNING: killing 13141 states (over memory cap)
KLEE: WARNING: killing 12739 states (over memory cap)
KLEE: WARNING: killing 13403 states (over memory cap)
KLEE: WARNING: killing 12666 states (over memory cap)
KLEE: WARNING: killing 12822 states (over memory cap)
KLEE: WARNING: killing 13035 states (over memory cap)
KLEE: WARNING: killing 12802 states (over memory cap)
KLEE: WARNING: killing 12731 states (over memory cap)
KLEE: WARNING: killing 12443 states (over memory cap)
KLEE: WARNING: killing 12263 states (over memory cap)
KLEE: WARNING: killing 13141 states (over memory cap)
KLEE: WARNING: killing 12794 states (over memory cap)
KLEE: WARNING: killing 12897 states (over memory cap)
KLEE: WARNING: killing 13053 states (over memory cap)
KLEE: WARNING: killing 12874 states (over memory cap)
KLEE: WARNING: killing 12638 states (over memory cap)
KLEE: WARNING: killing 12793 states (over memory cap)
KLEE: WARNING: killing 13116 states (over memory cap)
KLEE: WARNING: killing 13104 states (over memory cap)
KLEE: WARNING: killing 12325 states (over memory cap)
KLEE: WARNING: killing 12913 states (over memory cap)
KLEE: WARNING: killing 13019 states (over memory cap)
KLEE: WARNING: killing 13507 states (over memory cap)
KLEE: WARNING: killing 13166 states (over memory cap)
KLEE: WARNING: killing 13211 states (over memory cap)
KLEE: WARNING: killing 13259 states (over memory cap)
KLEE: WARNING: killing 12973 states (over memory cap)
KLEE: WARNING: killing 12684 states (over memory cap)
KLEE: WARNING: killing 12400 states (over memory cap)
KLEE: WARNING: killing 12601 states (over memory cap)
KLEE: WARNING: killing 12755 states (over memory cap)
KLEE: WARNING: killing 12792 states (over memory cap)
KLEE: WARNING: killing 12563 states (over memory cap)
KLEE: WARNING: killing 12884 states (over memory cap)
KLEE: WARNING: killing 13144 states (over memory cap)
KLEE: WARNING: killing 13139 states (over memory cap)
KLEE: WARNING: killing 12524 states (over memory cap)
KLEE: WARNING: killing 13063 states (over memory cap)
KLEE: WARNING: killing 13101 states (over memory cap)
KLEE: WARNING: killing 12925 states (over memory cap)
KLEE: WARNING: killing 12753 states (over memory cap)
KLEE: WARNING: killing 12852 states (over memory cap)
KLEE: WARNING: killing 13110 states (over memory cap)
KLEE: WARNING: killing 12884 states (over memory cap)
KLEE: WARNING: killing 13250 states (over memory cap)
KLEE: WARNING: killing 13020 states (over memory cap)
KLEE: WARNING: killing 12739 states (over memory cap)
KLEE: WARNING: killing 12944 states (over memory cap)
KLEE: WARNING: killing 12721 states (over memory cap)
KLEE: WARNING: killing 12710 states (over memory cap)
KLEE: WARNING: killing 12698 states (over memory cap)
KLEE: WARNING: killing 12792 states (over memory cap)
KLEE: WARNING: killing 13325 states (over memory cap)
KLEE: WARNING: killing 13151 states (over memory cap)
KLEE: WARNING: killing 12393 states (over memory cap)
KLEE: WARNING: killing 12754 states (over memory cap)
KLEE: WARNING: killing 12852 states (over memory cap)
KLEE: WARNING: killing 13001 states (over memory cap)
KLEE: WARNING: killing 12778 states (over memory cap)
KLEE: WARNING: killing 12926 states (over memory cap)
KLEE: WARNING: killing 12754 states (over memory cap)
KLEE: WARNING: killing 12688 states (over memory cap)
KLEE: WARNING: killing 12732 states (over memory cap)
KLEE: WARNING: killing 13044 states (over memory cap)
KLEE: WARNING: killing 13086 states (over memory cap)
