bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i.pp.i


--------------------------------------------------------------------------------


5.0.0-KLEE:86e6f6f8-dg:03407af1-symbiotic:a8aa8ad6-minisat:3db58943-stp:17249213-sbt-instrumentation:dd7e4312
INFO: After compilation stats: Globals/Functions/Blocks/Instr.: 1000 678 13502 78640
Removed infinite loop in receive_Data
Removed infinite loop in bm_bit_to_page_idx
Removed infinite loop in drbd_md_sync_page_io
Removed infinite loop in bm_word_to_page_idx
Removed infinite loop in bm_store_page_idx
Removed infinite loop in DCBP_set_code
Removed infinite loop in DCBP_set_pad_bits
Removed infinite loop in tl_hash_slot___0
Removed infinite loop in ee_hash_slot___0
Removed infinite loop in sg_assign_page
Removed infinite loop in bm_realloc_pages
Removed infinite loop in page_chain_add
Removed infinite loop in _bme_get
Removed infinite loop in page_chain_del
Removed infinite loop in vli_decode_bits
Removed infinite loop in ee_hash_slot
Removed infinite loop in tl_hash_slot
Removed infinite loop in _req_conflicts
Removed infinite loop in sg_assign_page___0
Removed infinite loop in w_make_resync_request
Removed infinite loop in drbd_try_rs_begin_io
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 2.40929389
Defining function seq_lseek as symbolic
Defining function seq_read as symbolic
Defining function single_release as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to 'prepare_to_wait' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Removed calls to 'force_sig' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'free_pages' (function is undefined)
Removed calls to '_raw_read_lock' (function is undefined)
Removed calls to '_raw_read_unlock' (function is undefined)
Defining function dev_err as symbolic
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Defining function lc_find as symbolic
Removed calls to '__wake_up' (function is undefined)
Removed calls to 'lc_destroy' (function is undefined)
Removed calls to '__free_pages' (function is undefined)
Removed calls to 'up' (function is undefined)
Defining function blkdev_put as symbolic
Defining function ___ratelimit as symbolic
Defining function dev_warn as symbolic
Defining function sock_recvmsg as symbolic
Defining function _dev_info as symbolic
Defining function sprintf as symbolic
Defining function mod_timer as symbolic
Removed calls to '_raw_write_lock_irq' (function is undefined)
Removed calls to '_raw_write_unlock_irq' (function is undefined)
Removed calls to 'complete' (function is undefined)
Removed calls to 'call_usermodehelper_setfns' (function is undefined)
Removed calls to 'get_random_bytes' (function is undefined)
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'lc_reset' (function is undefined)
Removed calls to 'flush_signals' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Defining function kthread_create_on_node as symbolic
Defining function wake_up_process as symbolic
Defining function ldv_undefined_int as symbolic
Removed calls to 'wait_for_completion' (function is undefined)
Defining function autoremove_wake_function as symbolic
Defining function kernel_sendmsg as symbolic
Defining function schedule_timeout_interruptible as symbolic
Removed calls to 'lc_del' (function is undefined)
Defining function dev_alert as symbolic
Defining function lc_element_by_index as symbolic
Defining function lc_put as symbolic
Defining function del_timer as symbolic
Removed calls to 'dump_stack' (function is undefined)
Removed calls to 'bio_endio' (function is undefined)
Removed calls to 'submit_bio' (function is undefined)
Removed calls to 'bio_put' (function is undefined)
Defining function bio_alloc as symbolic
Defining function bio_add_page as symbolic
Defining function printk as symbolic
Defining function mutex_trylock as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function _cond_resched as symbolic
Defining function blkdev_issue_flush as symbolic
Removed calls to 'put_page' (function is undefined)
Defining function alloc_pages_current as symbolic
Defining function __get_free_pages as symbolic
Defining function find_next_bit as symbolic
Defining function find_next_zero_bit as symbolic
Defining function random32 as symbolic
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to 'generic_make_request' (function is undefined)
Removed calls to 'lc_changed' (function is undefined)
Defining function bio_clone as symbolic
Defining function lc_index_of as symbolic
Defining function lc_get as symbolic
Removed calls to 'lock_acquire' (function is undefined)
Removed calls to 'part_round_stats' (function is undefined)
Removed calls to 'lock_release' (function is undefined)
Removed calls to 'mempool_free' (function is undefined)
Defining function cn_netlink_send as symbolic
Removed calls to 'sg_init_table' (function is undefined)
Defining function snprintf as symbolic
Defining function call_usermodehelper_setup as symbolic
Defining function call_usermodehelper_exec as symbolic
Removed calls to 'set_disk_ro' (function is undefined)
Defining function kobject_uevent as symbolic
Removed calls to 'blk_queue_logical_block_size' (function is undefined)
Removed calls to 'blk_queue_max_hw_sectors' (function is undefined)
Removed calls to 'blk_queue_max_segments' (function is undefined)
Removed calls to 'blk_queue_segment_boundary' (function is undefined)
Removed calls to 'blk_queue_stack_limits' (function is undefined)
Removed calls to 'vfree' (function is undefined)
Defining function vmalloc as symbolic
Defining function crypto_alloc_base as symbolic
Defining function schedule_timeout_uninterruptible as symbolic
Defining function mempool_alloc as symbolic
Removed calls to 'io_schedule' (function is undefined)
Defining function schedule_timeout as symbolic
Removed calls to 'free_cpumask_var' (function is undefined)
Defining function zalloc_cpumask_var as symbolic
Defining function __bitmap_parse as symbolic
Removed calls to 'add_disk' (function is undefined)
Defining function __bitmap_weight as symbolic
Defining function __bitmap_equal as symbolic
Defining function lc_create as symbolic
Removed calls to 'blk_queue_make_request' (function is undefined)
Removed calls to 'blk_queue_bounce_limit' (function is undefined)
Removed calls to 'blk_queue_merge_bvec' (function is undefined)
Removed calls to 'put_disk' (function is undefined)
Removed calls to 'blk_cleanup_queue' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'init_timer_key' (function is undefined)
Defining function blk_alloc_queue as symbolic
Defining function alloc_disk as symbolic
Defining function bdget as symbolic
Removed calls to 'bio_pair_release' (function is undefined)
Defining function bio_split as symbolic
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to 'add_timer' (function is undefined)
Removed calls to 'sock_release' (function is undefined)
Defining function set_cpus_allowed_ptr as symbolic
Defining function down_trylock as symbolic
Defining function down_interruptible as symbolic
Defining function kernel_sock_shutdown as symbolic
Defining function del_timer_sync as symbolic
Defining function __phys_addr as symbolic
Defining function mutex_lock_interruptible_nested as symbolic
Defining function sock_create_kern as symbolic
Defining function sock_create_lite as symbolic
Defining function lc_try_get as symbolic
Defining function blkdev_get_by_path as symbolic
Removed calls to 'lc_set' (function is undefined)
Removed calls to 'lc_seq_dump_details' (function is undefined)
Defining function single_open as symbolic
Defining function seq_printf as symbolic
Defining function lc_seq_printf_stats as symbolic
Removed calls to '__rwlock_init' (function is undefined)
Defining function register_blkdev as symbolic
Defining function register_reboot_notifier as symbolic
Defining function proc_create_data as symbolic
Removed calls to 'remove_proc_entry' (function is undefined)
Removed calls to 'cn_del_callback' (function is undefined)
Removed calls to 'del_gendisk' (function is undefined)
Removed calls to 'bdput' (function is undefined)
Removed calls to 'unregister_blkdev' (function is undefined)
Defining function unregister_reboot_notifier as symbolic
Removed calls to 'mempool_destroy' (function is undefined)
Removed calls to 'kmem_cache_destroy' (function is undefined)
Defining function kmem_cache_create as symbolic
Defining function mempool_alloc_slab as symbolic
Defining function mempool_create as symbolic
Defining function cn_add_callback as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'ldv_check_return_value' (function is undefined)
Linked our definitions to these undefined functions:
  memcmp
  strcmp
  strcpy
  strlen
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 2.61474108696
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 1160 472 5296 42750
INFO: Starting verification
KLEE: WARNING ONCE: function "receive_Data" has inline asm
KLEE: WARNING ONCE: function "receive_DataReply" has inline asm
KLEE: WARNING ONCE: function "receive_RSDataReply" has inline asm
KLEE: WARNING ONCE: function "receive_Barrier" has inline asm
KLEE: WARNING ONCE: function "receive_bitmap" has inline asm
KLEE: WARNING ONCE: function "receive_DataRequest" has inline asm
KLEE: WARNING ONCE: function "receive_protocol" has inline asm
KLEE: WARNING ONCE: function "receive_uuids" has inline asm
KLEE: WARNING ONCE: function "receive_sizes" has inline asm
KLEE: WARNING ONCE: function "receive_state" has inline asm
KLEE: WARNING ONCE: function "receive_sync_uuid" has inline asm
KLEE: WARNING ONCE: function "_get_ldev_if_state" has inline asm
KLEE: WARNING ONCE: function "put_ldev" has inline asm
KLEE: WARNING ONCE: function "drbd_ldev_destroy" has inline asm
KLEE: WARNING ONCE: function "drbd_go_diskless" has inline asm
KLEE: WARNING ONCE: function "__bm_print_lock_info" has inline asm
KLEE: WARNING ONCE: function "__bm_change_bits_to" has inline asm
KLEE: WARNING ONCE: function "drbd_recv" has inline asm
KLEE: WARNING ONCE: function "__drbd_set_state" has inline asm
KLEE: WARNING ONCE: function "is_valid_state" has inline asm
KLEE: WARNING ONCE: function "drbd_md_mark_dirty" has inline asm
KLEE: WARNING ONCE: function "_drbd_thread_stop" has inline asm
KLEE: WARNING ONCE: function "drbd_resume_al" has inline asm
KLEE: WARNING ONCE: function "w_after_state_ch" has inline asm
KLEE: WARNING ONCE: function "drbd_bcast_state" has inline asm
KLEE: WARNING ONCE: function "drbd_khelper" has inline asm
KLEE: WARNING ONCE: function "tl_clear" has inline asm
KLEE: WARNING ONCE: function "_tl_restart" has inline asm
KLEE: WARNING ONCE: function "drbd_send_state" has inline asm
KLEE: WARNING ONCE: function "drbd_queue_bitmap_io" has inline asm
KLEE: WARNING ONCE: function "drbd_bitmap_io_from_worker" has inline asm
KLEE: WARNING ONCE: function "drbd_md_sync" has inline asm
KLEE: WARNING ONCE: function "drbd_thread_start" has inline asm
KLEE: WARNING ONCE: function "drbd_thread_setup" has inline asm
KLEE: WARNING ONCE: function "drbd_start_resync" has inline asm
KLEE: WARNING ONCE: function "_drbd_request_state" has inline asm
KLEE: WARNING ONCE: function "drbd_req_state" has inline asm
KLEE: WARNING ONCE: function "drbd_state_lock___0" has inline asm
KLEE: WARNING ONCE: function "_req_st_cond" has inline asm
KLEE: WARNING ONCE: function "_drbd_send_cmd" has inline asm
KLEE: WARNING ONCE: function "drbd_send" has inline asm
KLEE: WARNING ONCE: function "we_should_drop_the_connection" has inline asm
KLEE: WARNING ONCE: function "request_ping" has inline asm
KLEE: WARNING ONCE: function "drbd_resync_finished" has inline asm
KLEE: WARNING ONCE: function "drbd_rs_del_all" has inline asm
KLEE: WARNING ONCE: function "drbd_md_sync_page_io" has inline asm
KLEE: WARNING ONCE: function "bm_rw" has inline asm
KLEE: WARNING ONCE: function "bm_page_io_async" has inline asm
KLEE: WARNING ONCE: function "bm_count_bits" has inline asm
KLEE: WARNING ONCE: function "__drbd_chk_io_error_" has inline asm
KLEE: WARNING ONCE: function "bm_store_page_idx" has inline asm
KLEE: WARNING ONCE: function "bm_async_io_complete" has inline asm
KLEE: WARNING ONCE: function "bm_memset" has inline asm
KLEE: WARNING ONCE: function "bm_clear_surplus" has inline asm
KLEE: WARNING ONCE: function "drbd_bm_lock" has inline asm
KLEE: WARNING ONCE: function "drbd_bm_get_lel" has inline asm
KLEE: WARNING ONCE: function "__bm_find_next" has inline asm
KLEE: WARNING ONCE: function "__req_mod" has inline asm
KLEE: WARNING ONCE: function "dec_ap_bio" has inline asm
KLEE: WARNING ONCE: function "drbd_get_max_buffers" has inline asm
KLEE: WARNING ONCE: function "put_net_conf" has inline asm
KLEE: WARNING ONCE: function "tl_hash_slot___0" has inline asm
KLEE: WARNING ONCE: function "queue_barrier" has inline asm
KLEE: WARNING ONCE: function "drbd_al_begin_io" has inline asm
KLEE: WARNING ONCE: function "_al_get" has inline asm
KLEE: WARNING ONCE: function "drbd_send_dblock" has inline asm
KLEE: WARNING ONCE: function "_drbd_send_page" has inline asm
KLEE: WARNING ONCE: function "sg_set_page" has inline asm
KLEE: WARNING ONCE: function "ee_hash_slot___0" has inline asm
KLEE: WARNING ONCE: function "_drbd_end_io_acct" has inline asm
KLEE: WARNING ONCE: function "drbd_bm_e_weight" has inline asm
KLEE: WARNING ONCE: function "drbd_bcast_sync_progress" has inline asm
KLEE: WARNING ONCE: function "drbd_bcast_ev_helper" has inline asm
KLEE: WARNING ONCE: function "drbd_set_role" has inline asm
KLEE: WARNING ONCE: function "drbd_bitmap_io" has inline asm
KLEE: WARNING ONCE: function "drbd_suspend_io" has inline asm
KLEE: WARNING ONCE: function "drbd_determine_dev_size" has inline asm
KLEE: WARNING ONCE: function "drbd_bm_resize" has inline asm
KLEE: WARNING ONCE: function "drbd_al_shrink" has inline asm
KLEE: WARNING ONCE: function "_drbd_send_ack" has inline asm
KLEE: WARNING ONCE: function "drbd_drain_block" has inline asm
KLEE: WARNING ONCE: function "w_e_end_data_req" has inline asm
KLEE: WARNING ONCE: function "w_e_end_rsdata_req" has inline asm
KLEE: WARNING ONCE: function "w_e_end_csum_rs_req" has inline asm
KLEE: WARNING ONCE: function "w_e_end_ov_reply" has inline asm
KLEE: WARNING ONCE: function "w_e_end_ov_req" has inline asm
KLEE: WARNING ONCE: function "drbd_rs_should_slow_down" has inline asm
KLEE: WARNING ONCE: function "drbd_rs_begin_io" has inline asm
KLEE: WARNING ONCE: function "drbd_pp_free" has inline asm
KLEE: WARNING ONCE: function "page_chain_add" has inline asm
KLEE: WARNING ONCE: function "drbd_endio_sec" has inline asm
KLEE: WARNING ONCE: function "__drbd_chk_io_error____0" has inline asm
KLEE: WARNING ONCE: function "_bme_get" has inline asm
KLEE: WARNING ONCE: function "move_to_net_ee_or_free" has inline asm
KLEE: WARNING ONCE: function "drbd_bm_count_bits" has inline asm
KLEE: WARNING ONCE: function "drbd_pp_alloc" has inline asm
KLEE: WARNING ONCE: function "drbd_pp_first_pages_or_try_alloc" has inline asm
KLEE: WARNING ONCE: function "drbd_bm_merge_lel" has inline asm
KLEE: WARNING ONCE: function "drbd_recv_header" has inline asm
KLEE: WARNING ONCE: function "bm_set_full_words_within_one_page" has inline asm
KLEE: WARNING ONCE: function "drbd_may_finish_epoch" has inline asm
KLEE: WARNING ONCE: function "_drbd_wait_ee_list_empty" has inline asm
KLEE: WARNING ONCE: function "read_in_block" has inline asm
KLEE: WARNING ONCE: function "e_end_resync_block" has inline asm
KLEE: WARNING ONCE: function "drbd_bcast_ee" has inline asm
KLEE: WARNING ONCE: function "e_end_block" has inline asm
KLEE: WARNING ONCE: function "tl_hash_slot" has inline asm
KLEE: WARNING ONCE: function "e_send_discard_ack" has inline asm
KLEE: WARNING ONCE: function "drbd_nl_disk_conf" has inline asm
KLEE: WARNING ONCE: function "drbd_nl_detach" has inline asm
KLEE: WARNING ONCE: function "drbd_nl_net_conf" has inline asm
KLEE: WARNING ONCE: function "drbd_nl_disconnect" has inline asm
KLEE: WARNING ONCE: function "drbd_nl_resize" has inline asm
KLEE: WARNING ONCE: function "drbd_nl_syncer_conf" has inline asm
KLEE: WARNING ONCE: function "drbd_nl_invalidate" has inline asm
KLEE: WARNING ONCE: function "drbd_nl_invalidate_peer" has inline asm
KLEE: WARNING ONCE: function "drbd_nl_resume_io" has inline asm
KLEE: WARNING ONCE: function "drbd_nl_get_config" has inline asm
KLEE: WARNING ONCE: function "drbd_nl_start_ov" has inline asm
KLEE: WARNING ONCE: function "drbd_suspend_al" has inline asm
KLEE: WARNING ONCE: function "drbd_calc_cpu_mask" has inline asm
KLEE: WARNING ONCE: function "w_resync_timer" has inline asm
KLEE: WARNING ONCE: function "w_bitmap_io" has inline asm
KLEE: WARNING ONCE: function "w_start_resync" has inline asm
KLEE: WARNING ONCE: function "request_timer_fn" has inline asm
KLEE: WARNING ONCE: function "drbdd_init" has inline asm
KLEE: WARNING ONCE: function "drbd_worker" has inline asm
KLEE: WARNING ONCE: function "drbd_asender" has inline asm
KLEE: WARNING ONCE: function "drbd_recv_short" has inline asm
KLEE: WARNING ONCE: function "drbd_thread_current_set_cpu" has inline asm
KLEE: WARNING ONCE: function "got_PingAck" has inline asm
KLEE: WARNING ONCE: function "got_BlockAck" has inline asm
KLEE: WARNING ONCE: function "got_NegAck" has inline asm
KLEE: WARNING ONCE: function "got_NegRSDReply" has inline asm
KLEE: WARNING ONCE: function "got_BarrierAck" has inline asm
KLEE: WARNING ONCE: function "got_RqSReply" has inline asm
KLEE: WARNING ONCE: function "got_OVResult" has inline asm
KLEE: WARNING ONCE: function "got_IsInSync" has inline asm
KLEE: WARNING ONCE: function "tl_release" has inline asm
KLEE: WARNING ONCE: function "drbd_mdev_cleanup" has inline asm
KLEE: WARNING ONCE: function "sg_set_buf" has inline asm
KLEE: WARNING ONCE: function "drbd_disconnect" has inline asm
KLEE: WARNING ONCE: function "drbd_rs_number_requests" has inline asm
KLEE: WARNING ONCE: function "drbd_try_rs_begin_io" has inline asm
KLEE: WARNING ONCE: function "drbd_bm_test_bit" has inline asm
KLEE: WARNING ONCE: function "w_e_send_csum" has inline asm
KLEE: WARNING ONCE: function "drbd_reconfig_start" has inline asm
KLEE: WARNING ONCE: function "drbd_reconfig_done" has inline asm
KLEE: WARNING ONCE: function "drbd_al_apply_to_bm" has inline asm
KLEE: WARNING ONCE: function "drbd_bm_ALe_set_all" has inline asm
KLEE: WARNING ONCE: function "drbd_resume_io" has inline asm
KLEE: WARNING ONCE: function "drbd_make_request" has inline asm
KLEE: WARNING ONCE: function "inc_ap_bio" has inline asm
KLEE: WARNING ONCE: function "drbd_make_request_common" has inline asm
KLEE: WARNING ONCE: function "inc_ap_bio_cond" has inline asm
KLEE: WARNING ONCE: function "drbd_connector_callback" 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/symbiotic-gwEf78/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i.pp.i:38231: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: flushing 32768 bytes on read, may be slow and/or crash: MO364[32768] allocated at global:__per_cpu_offset
KLEE: ERROR: /tmp/symbiotic-gwEf78/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i.pp.i:38231: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-gwEf78/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i.pp.i:38337: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-gwEf78/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i.pp.i:38339: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-gwEf78/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i.pp.i:11111: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
