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-thin-pool.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.: 233 401 2972 20442
Removed infinite loop in __pool_dec
Removed infinite loop in __pool_table_remove
Removed infinite loop in process_thin_deferred_cells
Removed infinite loop in get_next_mapping
Removed infinite loop in cmp_cells
Removed infinite loop in __pool_table_lookup
Removed infinite loop in __pool_inc
Removed infinite loop in __reserve_metadata_snap
Removed infinite loop in __pool_table_lookup_metadata_dev
Removed infinite loop in __pool_table_insert
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.694644927979
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to '__list_add_rcu' (function is undefined)
Removed calls to 'synchronize_sched' (function is undefined)
Removed calls to 'dm_put' (function is undefined)
Removed calls to 'down_write' (function is undefined)
Removed calls to 'up_write' (function is undefined)
Removed calls to 'dm_put_device' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to 'wait_for_completion' (function is undefined)
Removed calls to 'bio_endio' (function is undefined)
Removed calls to 'down_read' (function is undefined)
Removed calls to 'up_read' (function is undefined)
Removed calls to 'dm_deferred_entry_dec' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Defining function scnprintf as symbolic
Defining function printk as symbolic
Defining function sprintf as symbolic
Defining function dm_btree_lookup as symbolic
Defining function dm_btree_find_highest_key as symbolic
Removed calls to 'complete' (function is undefined)
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Defining function queue_work_on as symbolic
Defining function dm_noflush_suspending as symbolic
Removed calls to 'dm_cell_error' (function is undefined)
Removed calls to 'dm_bio_prison_free_cell' (function is undefined)
Removed calls to 'dm_cell_release_no_holder' (function is undefined)
Defining function dm_deferred_entry_inc as symbolic
Defining function dm_bio_prison_alloc_cell as symbolic
Defining function dm_bio_detain as symbolic
Removed calls to 'dm_bio_prison_destroy' (function is undefined)
Removed calls to 'dm_kcopyd_client_destroy' (function is undefined)
Removed calls to 'destroy_workqueue' (function is undefined)
Removed calls to 'mempool_free' (function is undefined)
Removed calls to 'mempool_destroy' (function is undefined)
Removed calls to 'dm_deferred_set_destroy' (function is undefined)
Removed calls to 'dm_tm_issue_prefetches' (function is undefined)
Removed calls to 'sort' (function is undefined)
Removed calls to 'rb_insert_color' (function is undefined)
Removed calls to 'rb_erase' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'blk_start_plug' (function is undefined)
Removed calls to 'blk_finish_plug' (function is undefined)
Removed calls to 'generic_make_request' (function is undefined)
Defining function dm_device_name as symbolic
Removed calls to 'dm_table_event' (function is undefined)
Removed calls to 'dm_bm_set_read_only' (function is undefined)
Removed calls to 'dm_bm_set_read_write' (function is undefined)
Removed calls to 'zero_fill_bio' (function is undefined)
Removed calls to 'dm_cell_visit_release' (function is undefined)
Defining function ___ratelimit as symbolic
Removed calls to 'dm_cell_release' (function is undefined)
Defining function dm_kcopyd_zero as symbolic
Defining function dm_deferred_set_add_work as symbolic
Defining function dm_kcopyd_copy as symbolic
Defining function queue_delayed_work_on as symbolic
Removed calls to 'dm_tm_inc' (function is undefined)
Defining function dm_btree_remove as symbolic
Defining function dm_btree_remove_leaves as symbolic
Defining function dm_btree_insert as symbolic
Removed calls to 'bio_chain' (function is undefined)
Removed calls to 'submit_bio' (function is undefined)
Removed calls to '___might_sleep' (function is undefined)
Defining function _cond_resched as symbolic
Defining function bio_alloc_bioset as symbolic
Defining function dm_btree_insert_notify as symbolic
Removed calls to 'lock_acquire' (function is undefined)
Removed calls to 'lockdep_rcu_suspicious' (function is undefined)
Defining function debug_lockdep_rcu_enabled as symbolic
Removed calls to 'lock_release' (function is undefined)
Defining function rcu_is_watching as symbolic
Defining function dm_block_data as symbolic
Defining function dm_bm_unlock as symbolic
Defining function dm_bm_write_lock as symbolic
Removed calls to 'dm_tm_destroy' (function is undefined)
Removed calls to 'dm_block_manager_destroy' (function is undefined)
Defining function dm_block_manager_create as symbolic
Defining function dm_bm_read_lock as symbolic
Defining function dm_tm_open_with_sm as symbolic
Defining function dm_sm_disk_open as symbolic
Defining function dm_tm_create_non_blocking_clone as symbolic
Defining function dm_btree_del as symbolic
Defining function dm_tm_create_with_sm as symbolic
Defining function dm_sm_disk_create as symbolic
Defining function dm_btree_empty as symbolic
Defining function dm_tm_pre_commit as symbolic
Defining function dm_tm_commit as symbolic
Defining function dm_bm_write_lock_zero as symbolic
Defining function dm_bm_block_size as symbolic
Defining function rb_first as symbolic
Defining function rb_next as symbolic
Defining function dm_bm_is_read_only as symbolic
Defining function dm_table_get_md as symbolic
Defining function dm_get_device as symbolic
Defining function dm_table_get_mode as symbolic
Defining function dm_get_md as symbolic
Defining function dm_set_target_max_io_len as symbolic
Defining function kstrtoull as symbolic
Removed calls to 'dm_consume_args' (function is undefined)
Removed calls to '__init_rwsem' (function is undefined)
Removed calls to 'init_timer_key' (function is undefined)
Removed calls to 'dm_table_add_target_callbacks' (function is undefined)
Removed calls to 'dm_internal_suspend_noflush' (function is undefined)
Removed calls to 'flush_workqueue' (function is undefined)
Removed calls to 'blk_limits_io_min' (function is undefined)
Removed calls to 'blk_limits_io_opt' (function is undefined)
Defining function bdevname as symbolic
Defining function strcasecmp as symbolic
Defining function dm_tm_read_lock as symbolic
Defining function dm_tm_unlock as symbolic
Removed calls to 'dm_tm_dec' (function is undefined)
Defining function dm_tm_shadow_block as symbolic
Defining function dm_block_location as symbolic
Defining function dm_suspended as symbolic
Removed calls to 'dm_internal_resume' (function is undefined)
Defining function cancel_delayed_work as symbolic
Defining function dm_bio_prison_create as symbolic
Defining function dm_kcopyd_client_create as symbolic
Defining function __alloc_workqueue_key as symbolic
Defining function dm_deferred_set_create as symbolic
Defining function mempool_alloc_slab as symbolic
Defining function mempool_create as symbolic
Defining function dm_read_arg_group as symbolic
Defining function dm_shift_arg as symbolic
Defining function dm_bm_checksum 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 '__mutex_init' (function is undefined)
Removed calls to 'ldv_check_final_state' (function is undefined)
Defining function ldv_resume_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_some_page as symbolic
Linked our definitions to these undefined functions:
  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.765478134155
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 371 292 1746 12554
INFO: Starting verification
KLEE: WARNING ONCE: function "__complete_mapping_preparation" has inline asm
KLEE: WARNING ONCE: function "thin_put" has inline asm
KLEE: WARNING ONCE: function "__pool_dec" has inline asm
KLEE: WARNING ONCE: function "do_worker" has inline asm
KLEE: WARNING ONCE: function "get_first_thin" has inline asm
KLEE: WARNING ONCE: function "get_next_thin" has inline asm
KLEE: WARNING ONCE: function "process_discard_cell_passdown" has inline asm
KLEE: WARNING ONCE: function "schedule_copy" has inline asm
KLEE: WARNING ONCE: function "get_next_mapping" has inline asm
KLEE: WARNING ONCE: function "rcu_read_lock" has inline asm
KLEE: WARNING ONCE: function "rcu_read_unlock" has inline asm
KLEE: WARNING ONCE: function "__pool_table_lookup" has inline asm
KLEE: WARNING ONCE: function "__pool_inc" has inline asm
KLEE: WARNING ONCE: function "pool_ctr" has inline asm
KLEE: WARNING ONCE: function "pool_io_hints" has inline asm
KLEE: WARNING ONCE: function "dm_pool_reserve_metadata_snap" has inline asm
KLEE: WARNING: undefined reference to function: delayed_work_timer_fn
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_d0461fe2-441b-41bc-ae0c-30360db6ac93/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8CrxpG/linux-4.2-rc1.tar.xz-43_2a-drivers--md--dm-thin-pool.ko-entry_point_true-unreach-call.cil.out.c:12688: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8CrxpG/linux-4.2-rc1.tar.xz-43_2a-drivers--md--dm-thin-pool.ko-entry_point_true-unreach-call.cil.out.c:12696: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8CrxpG/linux-4.2-rc1.tar.xz-43_2a-drivers--md--dm-thin-pool.ko-entry_point_true-unreach-call.cil.out.c:10207: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8CrxpG/linux-4.2-rc1.tar.xz-43_2a-drivers--md--dm-thin-pool.ko-entry_point_true-unreach-call.cil.out.c:10235: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8CrxpG/linux-4.2-rc1.tar.xz-43_2a-drivers--md--dm-thin-pool.ko-entry_point_true-unreach-call.cil.out.c:10796: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8CrxpG/linux-4.2-rc1.tar.xz-43_2a-drivers--md--dm-thin-pool.ko-entry_point_true-unreach-call.cil.out.c:10540: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8CrxpG/linux-4.2-rc1.tar.xz-43_2a-drivers--md--dm-thin-pool.ko-entry_point_true-unreach-call.cil.out.c:10824: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8CrxpG/linux-4.2-rc1.tar.xz-43_2a-drivers--md--dm-thin-pool.ko-entry_point_true-unreach-call.cil.out.c:9786: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8CrxpG/linux-4.2-rc1.tar.xz-43_2a-drivers--md--dm-thin-pool.ko-entry_point_true-unreach-call.cil.out.c:9536: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8CrxpG/linux-4.2-rc1.tar.xz-43_2a-drivers--md--dm-thin-pool.ko-entry_point_true-unreach-call.cil.out.c:10674: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8CrxpG/linux-4.2-rc1.tar.xz-43_2a-drivers--md--dm-thin-pool.ko-entry_point_true-unreach-call.cil.out.c:12705: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8CrxpG/linux-4.2-rc1.tar.xz-43_2a-drivers--md--dm-thin-pool.ko-entry_point_true-unreach-call.cil.out.c:12670: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8CrxpG/linux-4.2-rc1.tar.xz-43_2a-drivers--md--dm-thin-pool.ko-entry_point_true-unreach-call.cil.out.c:12670: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8CrxpG/linux-4.2-rc1.tar.xz-43_2a-drivers--md--dm-thin-pool.ko-entry_point_true-unreach-call.cil.out.c:9975: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8CrxpG/linux-4.2-rc1.tar.xz-43_2a-drivers--md--dm-thin-pool.ko-entry_point_true-unreach-call.cil.out.c:12671: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
