bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-fs--ceph--ceph.ko-ldv_main7_sequence_infinite_withcheck_stateful.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.: 1725 847 9335 78914
Removed infinite loop in ceph_handle_snapdir
Removed infinite loop in ceph_handle_notrace_create
Removed infinite loop in ceph_unreserve_caps
Removed infinite loop in __ceph_finish_cap_snap
Removed infinite loop in __ceph_flush_snaps
Removed infinite loop in __mark_caps_flushing
Removed infinite loop in __send_cap
Removed infinite loop in __ceph_build_xattrs_blob
Removed infinite loop in ceph_init_file
Removed infinite loop in ceph_put_fmode
Removed infinite loop in ceph_get_snapdir
Removed infinite loop in ceph_mdsmap_get_state
Removed infinite loop in create_request_message
Removed infinite loop in ceph_encode_filepath
Removed infinite loop in ceph_choose_frag
Removed infinite loop in ceph_reserve_caps
Removed infinite loop in __insert_request
Removed infinite loop in ceph_readdir
Removed infinite loop in try_flush_caps
Removed infinite loop in __ceph_mark_dirty_caps
Removed infinite loop in ceph_writepage
Removed infinite loop in ceph_writepages_start
Removed infinite loop in ceph_set_page_dirty
Removed infinite loop in ceph_readpages
Removed infinite loop in ceph_invalidatepage
Removed infinite loop in ceph_put_wrbuffer_cap_refs
Removed infinite loop in zero_user_segments
Removed infinite loop in ceph_update_writeable_page
Removed infinite loop in start_read
Removed infinite loop in writepages_finish
Removed infinite loop in __unregister_session
Removed infinite loop in remove_session_caps
Removed infinite loop in iterate_session_caps
Removed infinite loop in ceph_put_cap
Removed infinite loop in ceph_fs_debugfs_init
Removed infinite loop in ceph_adjust_min_caps
Removed infinite loop in parse_fsopt_token
Removed infinite loop in __free_xattr
Removed infinite loop in __queue_cap_release
Removed infinite loop in handle_forward
Removed infinite loop in __insert_snap_realm
Removed infinite loop in handle_cap_grant
Removed infinite loop in handle_cap_flush_ack
Removed infinite loop in get_cap
Removed infinite loop in __insert_cap_node
Removed infinite loop in ceph_fill_trace
Removed infinite loop in splice_dentry
Removed infinite loop in ceph_set_dentry_offset
Removed infinite loop in ceph_vxattrs_name_size
Removed infinite loop in ceph_mdsc_lease_release
INFO: Compilation, preparation and instrumentation time: 2.45019888878
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'd_drop' (function is undefined)
Removed calls to 'ihold' (function is undefined)
Removed calls to 'd_instantiate' (function is undefined)
Removed calls to 'd_delete' (function is undefined)
Removed calls to 'd_move' (function is undefined)
Removed calls to '__mark_inode_dirty' (function is undefined)
Removed calls to 'iput' (function is undefined)
Removed calls to 'generic_fillattr' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to '__free_pages' (function is undefined)
Removed calls to 'rb_erase' (function is undefined)
Removed calls to 'kmem_cache_free' (function is undefined)
Removed calls to 'd_set_d_op' (function is undefined)
Removed calls to 'd_rehash' (function is undefined)
Defining function finish_no_open as symbolic
Defining function finish_open as symbolic
Removed calls to 'dput' (function is undefined)
Removed calls to 'ceph_msg_last_put' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to 'up_read' (function is undefined)
Removed calls to 'down_read' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'ceph_con_send' (function is undefined)
Removed calls to 'ceph_buffer_release' (function is undefined)
Defining function ceph_msg_new as symbolic
Defining function rb_first as symbolic
Defining function down_read_trylock as symbolic
Defining function rb_next as symbolic
Defining function queue_work as symbolic
Defining function mutex_trylock as symbolic
Defining function round_jiffies as symbolic
Defining function invalidate_mapping_pages as symbolic
Defining function ceph_caps_for_mode as symbolic
Defining function ceph_flags_to_mode as symbolic
Defining function kmem_cache_alloc as symbolic
Removed calls to 'unlock_new_inode' (function is undefined)
Defining function iget5_locked as symbolic
Removed calls to 'rb_insert_color' (function is undefined)
Removed calls to 'get_random_bytes' (function is undefined)
Removed calls to 'complete_all' (function is undefined)
Defining function wait_for_completion_killable_timeout as symbolic
Defining function wait_for_completion_killable as symbolic
Defining function d_find_any_alias as symbolic
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'ceph_con_init' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'ceph_con_open' (function is undefined)
Removed calls to 'lock_acquire' (function is undefined)
Removed calls to 'lockdep_rcu_suspicious' (function is undefined)
Removed calls to 'lock_release' (function is undefined)
Defining function printk as symbolic
Defining function debug_lockdep_rcu_enabled as symbolic
Defining function rcu_is_cpu_idle as symbolic
Defining function d_find_alias as symbolic
Defining function ceph_str_hash as symbolic
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'might_fault' (function is undefined)
Removed calls to 'wait_for_completion' (function is undefined)
Defining function filemap_write_and_wait_range as symbolic
Defining function wait_for_completion_timeout as symbolic
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Defining function ceph_calc_file_object_mapping as symbolic
Defining function snprintf as symbolic
Defining function ceph_calc_object_layout as symbolic
Defining function ceph_calc_pg_primary as symbolic
Defining function _copy_to_user as symbolic
Defining function _copy_from_user as symbolic
Defining function kstrdup as symbolic
Defining function do_sync_read as symbolic
Defining function do_sync_write as symbolic
Removed calls to 'ceph_zero_page_vector_range' (function is undefined)
Removed calls to 'ceph_put_page_vector' (function is undefined)
Removed calls to 'ceph_release_page_vector' (function is undefined)
Removed calls to 'truncate_inode_pages_range' (function is undefined)
Removed calls to 'touch_atime' (function is undefined)
Removed calls to 'prepare_to_wait' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Defining function generic_file_splice_write as symbolic
Defining function generic_file_splice_read as symbolic
Defining function flock_lock_file_wait as symbolic
Defining function posix_lock_file as symbolic
Defining function autoremove_wake_function as symbolic
Removed calls to 'ceph_osdc_release_request' (function is undefined)
Removed calls to 'truncate_inode_pages' (function is undefined)
Defining function generic_file_aio_write as symbolic
Defining function vfs_fsync_range as symbolic
Defining function current_kernel_time as symbolic
Defining function invalidate_inode_pages2_range as symbolic
Defining function ceph_osdc_new_request as symbolic
Defining function ceph_get_direct_page_vector as symbolic
Defining function ceph_alloc_page_vector as symbolic
Defining function ceph_copy_user_to_page_vector as symbolic
Defining function ceph_osdc_start_request as symbolic
Defining function ceph_osdc_wait_request as symbolic
Defining function generic_file_aio_read as symbolic
Defining function filemap_write_and_wait as symbolic
Defining function ceph_copy_page_vector_to_user as symbolic
Defining function ceph_osdc_readpages as symbolic
Removed calls to 'unlock_page' (function is undefined)
Removed calls to 'wait_on_page_bit' (function is undefined)
Removed calls to 'set_bdi_congested' (function is undefined)
Removed calls to '__pagevec_release' (function is undefined)
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to 'account_page_dirtied' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to 'put_page' (function is undefined)
Defining function set_page_dirty as symbolic
Defining function grab_cache_page_write_begin as symbolic
Defining function clear_page_dirty_for_io as symbolic
Removed calls to 'end_page_writeback' (function is undefined)
Defining function ceph_osdc_writepages as symbolic
Defining function test_set_page_writeback as symbolic
Defining function add_to_page_cache_lru as symbolic
Defining function radix_tree_tag_set as symbolic
Defining function pagevec_lookup_tag as symbolic
Removed calls to '__lock_page' (function is undefined)
Removed calls to 'clear_bdi_congested' (function is undefined)
Removed calls to 'mempool_free' (function is undefined)
Defining function generic_error_remove_page as symbolic
Defining function mempool_alloc as symbolic
Defining function d_obtain_alias as symbolic
Defining function ilookup5 as symbolic
Removed calls to 'destroy_workqueue' (function is undefined)
Removed calls to 'bdi_destroy' (function is undefined)
Removed calls to 'ceph_destroy_client' (function is undefined)
Removed calls to 'ceph_destroy_options' (function is undefined)
Removed calls to 'deactivate_locked_super' (function is undefined)
Removed calls to 'kill_anon_super' (function is undefined)
Removed calls to 'ceph_msgr_flush' (function is undefined)
Removed calls to 'mempool_destroy' (function is undefined)
Removed calls to 'debugfs_remove' (function is undefined)
Defining function cancel_delayed_work_sync as symbolic
Removed calls to '__init_rwsem' (function is undefined)
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to 'init_timer_key' (function is undefined)
Defining function sget as symbolic
Removed calls to 'down_write' (function is undefined)
Removed calls to 'up_write' (function is undefined)
Defining function schedule_timeout as symbolic
Removed calls to 'ceph_con_close' (function is undefined)
Defining function igrab as symbolic
Defining function down_write_trylock as symbolic
Defining function __ceph_open_session as symbolic
Defining function debugfs_create_file as symbolic
Defining function debugfs_create_symlink as symbolic
Defining function d_make_root as symbolic
Defining function bdi_register as symbolic
Defining function set_anon_super as symbolic
Removed calls to 'ceph_con_keepalive' (function is undefined)
Defining function round_jiffies_relative as symbolic
Defining function schedule_delayed_work as symbolic
Defining function ceph_create_client as symbolic
Defining function bdi_init as symbolic
Defining function __alloc_workqueue_key as symbolic
Defining function mempool_kmalloc as symbolic
Defining function mempool_create as symbolic
Defining function ceph_check_fsid as symbolic
Defining function ceph_monc_got_mdsmap as symbolic
Removed calls to 'print_hex_dump' (function is undefined)
Removed calls to 'ceph_pagelist_set_cursor' (function is undefined)
Removed calls to 'lock_flocks' (function is undefined)
Removed calls to 'unlock_flocks' (function is undefined)
Defining function ceph_pagelist_append as symbolic
Defining function ceph_pagelist_release as symbolic
Defining function ceph_pagelist_truncate as symbolic
Defining function ceph_pagelist_reserve as symbolic
Defining function ceph_pr_addr as symbolic
Defining function ceph_parse_options as symbolic
Defining function match_token as symbolic
Defining function match_int as symbolic
Defining function kstrndup as symbolic
Defining function int_sqrt as symbolic
Defining function ceph_compare_options as symbolic
Removed calls to 'call_rcu_sched' (function is undefined)
Removed calls to 'bdi_unregister' (function is undefined)
Removed calls to 'ceph_osdc_sync' (function is undefined)
Defining function seq_printf as symbolic
Defining function seq_puts as symbolic
Defining function ceph_monc_do_statfs as symbolic
Defining function filemap_fdatawrite as symbolic
Defining function generic_readlink as symbolic
Defining function filemap_fault as symbolic
Defining function generic_file_remap_pages as symbolic
Defining function file_update_time as symbolic
Removed calls to 'ceph_msg_dump' (function is undefined)
Removed calls to 'downgrade_write' (function is undefined)
Defining function ceph_monc_validate_auth as symbolic
Removed calls to 'set_nlink' (function is undefined)
Defining function ceph_msg_type_name as symbolic
Defining function full_name_hash as symbolic
Defining function d_lookup as symbolic
Removed calls to 'sort' (function is undefined)
Removed calls to '_raw_spin_lock_nested' (function is undefined)
Defining function d_alloc as symbolic
Removed calls to 'init_special_inode' (function is undefined)
Defining function ceph_buffer_new as symbolic
Defining function d_materialise_unique as symbolic
Removed calls to 'd_prune_aliases' (function is undefined)
Defining function generic_file_llseek as symbolic
Defining function simple_attr_read as symbolic
Defining function simple_attr_write as symbolic
Defining function simple_attr_release as symbolic
Defining function simple_attr_open as symbolic
Defining function seq_lseek as symbolic
Defining function seq_read as symbolic
Defining function single_release as symbolic
Defining function single_open as symbolic
Defining function kmemdup as symbolic
Defining function __page_cache_alloc as symbolic
Defining function inode_change_ok as symbolic
Defining function generic_permission as symbolic
Removed calls to 'ldv_handler_precall' (function is undefined)
Removed calls to 'kmem_cache_destroy' (function is undefined)
Defining function unregister_filesystem as symbolic
Removed calls to 'rcu_barrier' (function is undefined)
Defining function register_filesystem as symbolic
Removed calls to 'inode_init_once' (function is undefined)
Defining function kmem_cache_create as symbolic
Removed calls to 'ldv_check_return_value' (function is undefined)
Linked our definitions to these undefined functions:
  memcmp
  strchr
  strcmp
  strlen
  strncmp
  strncpy
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 2.39551091194
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 1191 707 5116 46367
INFO: Starting verification
KLEE: WARNING ONCE: function "ceph_listxattr" has inline asm
KLEE: WARNING ONCE: function "ceph_init_dentry" has inline asm
KLEE: WARNING ONCE: function "ceph_handle_snapdir" has inline asm
KLEE: WARNING ONCE: function "ceph_handle_notrace_create" has inline asm
KLEE: WARNING ONCE: function "ceph_mdsc_put_request" has inline asm
KLEE: WARNING ONCE: function "ceph_msg_put" has inline asm
KLEE: WARNING ONCE: function "ceph_put_mds_session" has inline asm
KLEE: WARNING ONCE: function "ceph_unreserve_caps" has inline asm
KLEE: WARNING ONCE: function "__ceph_finish_cap_snap" has inline asm
KLEE: WARNING ONCE: function "__ceph_flush_snaps" has inline asm
KLEE: WARNING ONCE: function "send_cap_msg" has inline asm
KLEE: WARNING ONCE: function "ceph_put_cap_snap" has inline asm
KLEE: WARNING ONCE: function "ceph_buffer_put" has inline asm
KLEE: WARNING ONCE: function "get_session" has inline asm
KLEE: WARNING ONCE: function "__mark_caps_flushing" has inline asm
KLEE: WARNING ONCE: function "__send_cap" has inline asm
KLEE: WARNING ONCE: function "__ceph_build_xattrs_blob" has inline asm
KLEE: WARNING ONCE: function "ceph_init_file" has inline asm
KLEE: WARNING ONCE: function "ceph_put_fmode" has inline asm
KLEE: WARNING ONCE: function "ceph_get_snapdir" has inline asm
KLEE: WARNING ONCE: function "__register_request" has inline asm
KLEE: WARNING ONCE: function "__do_request" has inline asm
KLEE: WARNING ONCE: function "ceph_dir_clear_complete" has inline asm
KLEE: WARNING ONCE: function "ceph_mdsmap_get_state" has inline asm
KLEE: WARNING ONCE: function "ceph_choose_frag" has inline asm
KLEE: WARNING ONCE: function "register_session" has inline asm
KLEE: WARNING ONCE: function "__prepare_send_request" has inline asm
KLEE: WARNING ONCE: function "ceph_encode_filepath" has inline asm
KLEE: WARNING ONCE: function "ceph_mdsc_build_path" 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 "ceph_reserve_caps" has inline asm
KLEE: WARNING ONCE: function "ceph_readdir" has inline asm
KLEE: WARNING ONCE: function "ceph_dir_fsync" has inline asm
KLEE: WARNING ONCE: function "ceph_dir_test_complete" has inline asm
KLEE: WARNING ONCE: function "ceph_dir_set_complete" has inline asm
KLEE: WARNING ONCE: function "ceph_d_revalidate" has inline asm
KLEE: WARNING ONCE: function "ceph_d_prune" has inline asm
KLEE: WARNING ONCE: function "ceph_fsync" has inline asm
KLEE: WARNING ONCE: function "ceph_lock" has inline asm
KLEE: WARNING ONCE: function "ceph_flock" has inline asm
KLEE: WARNING ONCE: function "ceph_osdc_put_request" has inline asm
KLEE: WARNING ONCE: function "try_flush_caps" has inline asm
KLEE: WARNING ONCE: function "ceph_get_caps" has inline asm
KLEE: WARNING ONCE: function "__ceph_mark_dirty_caps" has inline asm
KLEE: WARNING ONCE: function "ceph_writepage" has inline asm
KLEE: WARNING ONCE: function "ceph_writepages_start" has inline asm
KLEE: WARNING ONCE: function "ceph_set_page_dirty" has inline asm
KLEE: WARNING ONCE: function "ceph_readpages" has inline asm
KLEE: WARNING ONCE: function "ceph_write_end" has inline asm
KLEE: WARNING ONCE: function "ceph_invalidatepage" has inline asm
KLEE: WARNING ONCE: function "ceph_put_wrbuffer_cap_refs" has inline asm
KLEE: WARNING ONCE: function "ceph_put_snap_context" has inline asm
KLEE: WARNING ONCE: function "zero_user_segments" has inline asm
KLEE: WARNING ONCE: function "ceph_update_writeable_page" has inline asm
KLEE: WARNING ONCE: function "get_oldest_context" has inline asm
KLEE: WARNING ONCE: function "writepage_nounlock" has inline asm
KLEE: WARNING ONCE: function "readpage_nounlock" has inline asm
KLEE: WARNING ONCE: function "finish_read" has inline asm
KLEE: WARNING ONCE: function "lock_page" has inline asm
KLEE: WARNING ONCE: function "writepages_finish" has inline asm
KLEE: WARNING ONCE: function "ceph_mount" has inline asm
KLEE: WARNING ONCE: function "parse_fsopt_token" has inline asm
KLEE: WARNING ONCE: function "ceph_fs_debugfs_init" has inline asm
KLEE: WARNING ONCE: function "ceph_mdsc_close_sessions" has inline asm
KLEE: WARNING ONCE: function "__unregister_session" has inline asm
KLEE: WARNING ONCE: function "remove_session_caps" has inline asm
KLEE: WARNING ONCE: function "__destroy_snap_realm" has inline asm
KLEE: WARNING ONCE: function "iterate_session_caps" has inline asm
KLEE: WARNING ONCE: function "ceph_put_cap" has inline asm
KLEE: WARNING ONCE: function "ceph_put_snap_realm" has inline asm
KLEE: WARNING ONCE: function "ceph_adjust_min_caps" has inline asm
KLEE: WARNING ONCE: function "send_mds_reconnect" has inline asm
KLEE: WARNING ONCE: function "ceph_write_inode" has inline asm
KLEE: WARNING ONCE: function "ceph_mdsc_sync" has inline asm
KLEE: WARNING ONCE: function "__queue_cap_release" has inline asm
KLEE: WARNING ONCE: function "dispatch" has inline asm
KLEE: WARNING ONCE: function "__lookup_request" has inline asm
KLEE: WARNING ONCE: function "ceph_fill_trace" has inline asm
KLEE: WARNING ONCE: function "ceph_handle_caps" has inline asm
KLEE: WARNING ONCE: function "ceph_create_snap_realm" has inline asm
KLEE: WARNING ONCE: function "ceph_get_snap_realm" has inline asm
KLEE: WARNING ONCE: function "ceph_add_cap" has inline asm
KLEE: WARNING ONCE: function "splice_dentry" has inline asm
KLEE: WARNING ONCE: function "fill_inode" has inline asm
KLEE: WARNING ONCE: function "update_dentry_lease" has inline asm
KLEE: WARNING ONCE: function "ceph_set_dentry_offset" has inline asm
KLEE: WARNING ONCE: function "ceph_queue_cap_snap" has inline asm
KLEE: WARNING ONCE: function "ceph_mdsc_lease_release" has inline asm
KLEE: WARNING: undefined reference to function: delayed_work_timer_fn
KLEE: WARNING: undefined reference to function: mempool_kfree
KLEE: WARNING ONCE: flushing 9576 bytes on read, may be slow and/or crash: MO220[9576] allocated at global:
KLEE: ERROR: /tmp/symbiotic-xPhFKy/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-fs--ceph--ceph.ko-ldv_main7_sequence_infinite_withcheck_stateful.cil.out.c:4728: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xPhFKy/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-fs--ceph--ceph.ko-ldv_main7_sequence_infinite_withcheck_stateful.cil.out.c:20842: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xPhFKy/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-fs--ceph--ceph.ko-ldv_main7_sequence_infinite_withcheck_stateful.cil.out.c:20979: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xPhFKy/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-fs--ceph--ceph.ko-ldv_main7_sequence_infinite_withcheck_stateful.cil.out.c:7003: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xPhFKy/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-fs--ceph--ceph.ko-ldv_main7_sequence_infinite_withcheck_stateful.cil.out.c:21113: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
