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--staging--lustre--lustre--llite--lustre.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.: 1844 1441 16184 126255
Removed infinite loop in get_page
Removed infinite loop in page_mapcount
Removed infinite loop in get_page___0
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 4.51366710663
Removed calls to 'lbug_with_loc' (function is undefined)
Removed calls to 'call_rcu_sched' (function is undefined)
Removed calls to 'lprocfs_counter_add' (function is undefined)
Removed calls to 'ccc_inode_lsm_put' (function is undefined)
Removed calls to 'clear_nlink' (function is undefined)
Removed calls to 'iput' (function is undefined)
Defining function libcfs_debug_msg as symbolic
Defining function lov_lsm_get as symbolic
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function generic_read_dir as symbolic
Removed calls to '__might_fault' (function is undefined)
Removed calls to 'ptlrpc_req_finished' (function is undefined)
Removed calls to 'kvfree' (function is undefined)
Defining function filemap_write_and_wait_range as symbolic
Defining function lov_read_and_clear_async_rc as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to '_debug_capa' (function is undefined)
Removed calls to 'lprocfs_counter_sub' (function is undefined)
Removed calls to 'kmem_cache_free' (function is undefined)
Removed calls to 'cl_io_fini' (function is undefined)
Removed calls to 'cl_env_nested_put' (function is undefined)
Defining function cl_env_nested_get as symbolic
Defining function cl_io_init as symbolic
Defining function cl_io_loop as symbolic
Defining function lu_context_key_get as symbolic
Defining function debug_lockdep_rcu_enabled as symbolic
Defining function from_kgid as symbolic
Removed calls to 'libcfs_debug_dumplog' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Removed calls to 'add_wait_queue' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'cfs_clear_sigpending' (function is undefined)
Removed calls to 'cfs_restore_sigs' (function is undefined)
Removed calls to 'remove_wait_queue' (function is undefined)
Defining function __cfs_fail_timeout_set as symbolic
Removed calls to 'unlock_res_and_lock' (function is undefined)
Removed calls to 'ldlm_lock_put' (function is undefined)
Defining function class_exp2obd as symbolic
Removed calls to 'md_from_obdo' (function is undefined)
Defining function req_capsule_server_get as symbolic
Removed calls to '__list_add' (function is undefined)
Defining function req_capsule_server_sized_get as symbolic
Defining function obd_alloc_fail as symbolic
Defining function __cfs_fail_check_set as symbolic
Removed calls to 'obdo_refresh_inode' (function is undefined)
Removed calls to 'ptlrpc_set_destroy' (function is undefined)
Defining function ptlrpc_prep_set as symbolic
Defining function ptlrpc_set_wait as symbolic
Defining function get_seconds as symbolic
Defining function from_kuid as symbolic
Defining function cfs_curproc_cap_pack as symbolic
Defining function in_group_p as symbolic
Defining function igrab as symbolic
Removed calls to 'cl_unuse' (function is undefined)
Removed calls to 'cl_lock_release' (function is undefined)
Removed calls to 'cl_env_put' (function is undefined)
Defining function cl_lock_peek as symbolic
Removed calls to 'cl_object_attr_lock' (function is undefined)
Removed calls to 'cl_object_attr_unlock' (function is undefined)
Defining function cl_object_attr_get as symbolic
Defining function cl_env_get as symbolic
Defining function lock_res_and_lock as symbolic
Defining function ldlm_cli_cancel as symbolic
Defining function __ldlm_handle2lock as symbolic
Removed calls to 'cl_env_implant' (function is undefined)
Defining function cfs_block_sigsinv as symbolic
Defining function schedule_timeout as symbolic
Defining function cfs_signal_pending as symbolic
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to 'ldlm_lock_decref' (function is undefined)
Defining function it_disposition as symbolic
Defining function default_wake_function as symbolic
Removed calls to 'list_del' (function is undefined)
Removed calls to 'lustre_ext_acl_xattr_free' (function is undefined)
Removed calls to 'it_clear_disposition' (function is undefined)
Defining function it_open_error as symbolic
Removed calls to 'ldlm_lock2handle' (function is undefined)
Removed calls to '_ldlm_lock_debug' (function is undefined)
Removed calls to 'down_write' (function is undefined)
Removed calls to 'up_write' (function is undefined)
Removed calls to 'truncate_inode_pages' (function is undefined)
Removed calls to '__d_drop' (function is undefined)
Removed calls to 'set_nlink' (function is undefined)
Removed calls to 'make_bad_inode' (function is undefined)
Removed calls to 'unlock_new_inode' (function is undefined)
Removed calls to 'kfree_call_rcu' (function is undefined)
Removed calls to 'ldlm_lock_allow_match' (function is undefined)
Defining function cl_conf_set as symbolic
Defining function iget5_locked as symbolic
Removed calls to 'init_special_inode' (function is undefined)
Defining function cl_object_find as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to '__init_rwsem' (function is undefined)
Defining function make_kuid as symbolic
Defining function make_kgid as symbolic
Defining function mod_timer as symbolic
Removed calls to 'obdo_set_parent_fid' (function is undefined)
Defining function obd_ioctl_getdata as symbolic
Removed calls to '__copy_from_user_overflow' (function is undefined)
Removed calls to '__copy_to_user_overflow' (function is undefined)
Defining function libcfs_kvzalloc as symbolic
Defining function capable as symbolic
Defining function memdup_user as symbolic
Removed calls to 'ldlm_lock_decref_and_cancel' (function is undefined)
Defining function ilookup5 as symbolic
Defining function in_egroup_p as symbolic
Defining function strncpy_from_user as symbolic
Defining function _copy_to_user as symbolic
Defining function sprintf as symbolic
Defining function _copy_from_user as symbolic
Defining function current_umask as symbolic
Removed calls to 'put_page' (function is undefined)
Removed calls to 'ldlm_lock_dump_handle' (function is undefined)
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to 'dump_page' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Removed calls to 'wait_on_page_bit' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'unlock_page' (function is undefined)
Removed calls to '__lock_page' (function is undefined)
Removed calls to 'cancel_dirty_page' (function is undefined)
Removed calls to 'delete_from_page_cache' (function is undefined)
Defining function ldlm_completion_ast as symbolic
Defining function read_cache_page as symbolic
Defining function add_to_page_cache_lru as symbolic
Defining function __page_cache_alloc as symbolic
Defining function radix_tree_gang_lookup as symbolic
Defining function __get_page_tail as symbolic
Removed calls to 'fput' (function is undefined)
Removed calls to 'down_read' (function is undefined)
Removed calls to 'up_read' (function is undefined)
Defining function cl_io_rw_init as symbolic
Defining function mutex_lock_interruptible_nested as symbolic
Defining function generic_file_mmap as symbolic
Defining function cl_lock_request as symbolic
Defining function cl_wait as symbolic
Defining function radix_tree_gang_lookup_tag as symbolic
Defining function lu_object_locate as symbolic
Defining function fget as symbolic
Removed calls to 'inode_dio_wait' (function is undefined)
Defining function inode_newsize_ok as symbolic
Defining function current_kernel_time as symbolic
Defining function simple_setattr as symbolic
Removed calls to 'cl_env_unplant' (function is undefined)
Removed calls to 'obdo_from_inode' (function is undefined)
Defining function filemap_fdatawrite as symbolic
Defining function inode_permission as symbolic
Defining function generic_file_llseek_size as symbolic
Defining function ldlm_flock_completion_ast as symbolic
Defining function flock_lock_file_wait as symbolic
Defining function posix_lock_file_wait as symbolic
Removed calls to 'lustre_posix_acl_xattr_free' (function is undefined)
Defining function inode_owner_or_capable as symbolic
Defining function selinux_is_enabled as symbolic
Defining function lustre_acl_xattr_merge2ext as symbolic
Defining function lustre_posix_acl_xattr_filter as symbolic
Defining function strnlen as symbolic
Defining function __memmove as symbolic
Defining function posix_acl_to_xattr as symbolic
Removed calls to 'downgrade_write' (function is undefined)
Defining function lustre_posix_acl_xattr_2ext as symbolic
Defining function kstrdup as symbolic
Defining function kmemdup as symbolic
Defining function generic_permission as symbolic
Defining function req_capsule_server_swab_get as symbolic
Defining function is_bad_inode as symbolic
Defining function d_obtain_alias as symbolic
Removed calls to 'd_move' (function is undefined)
Removed calls to 'd_instantiate' (function is undefined)
Removed calls to 'dput' (function is undefined)
Defining function finish_no_open as symbolic
Defining function finish_open as symbolic
Defining function ldlm_it2str as symbolic
Removed calls to 'd_rehash' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'lockref_get' (function is undefined)
Defining function kthread_create_on_node as symbolic
Defining function wake_up_process as symbolic
Defining function d_lookup as symbolic
Defining function ptlrpc_request_addref as symbolic
Defining function full_name_hash as symbolic
Defining function down_write_trylock as symbolic
Defining function generic_readlink as symbolic
Removed calls to 'cl_2queue_init' (function is undefined)
Removed calls to 'cl_page_put' (function is undefined)
Removed calls to 'cl_page_disown' (function is undefined)
Removed calls to 'cl_2queue_add' (function is undefined)
Removed calls to 'cl_page_clip' (function is undefined)
Removed calls to 'cl_2queue_discard' (function is undefined)
Removed calls to 'cl_2queue_disown' (function is undefined)
Removed calls to 'cl_2queue_fini' (function is undefined)
Defining function cl_page_size as symbolic
Defining function cl_index as symbolic
Defining function cl_page_find as symbolic
Defining function cl_page_own as symbolic
Defining function cl_page_vmpage as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function set_page_dirty as symbolic
Defining function cl_io_submit_sync as symbolic
Removed calls to 'cl_page_assume' (function is undefined)
Removed calls to 'cl_page_delete' (function is undefined)
Removed calls to 'iov_iter_advance' (function is undefined)
Removed calls to 'lov_stripe_lock' (function is undefined)
Removed calls to 'lov_stripe_unlock' (function is undefined)
Defining function iov_iter_alignment as symbolic
Defining function iov_iter_get_pages_alloc as symbolic
Defining function set_page_dirty_lock as symbolic
Defining function cl_vmpage_page as symbolic
Removed calls to 'cl_page_unassume' (function is undefined)
Defining function cl_page_is_owned as symbolic
Defining function cl_io_commit_write as symbolic
Defining function grab_cache_page_write_begin as symbolic
Removed calls to 'cl_page_get' (function is undefined)
Removed calls to 'dump_stack' (function is undefined)
Defining function cl_io_prepare_write as symbolic
Defining function mutex_trylock as symbolic
Defining function cl_io_iter_init as symbolic
Defining function cl_io_lock as symbolic
Defining function cl_io_start as symbolic
Defining function __set_page_dirty_nobuffers as symbolic
Defining function cl_io_read_page as symbolic
Defining function cl_page_flush as symbolic
Defining function redirty_page_for_writepage as symbolic
Defining function cl_offset as symbolic
Removed calls to 'inode_init_once' (function is undefined)
Removed calls to 'truncate_inode_pages_final' (function is undefined)
Removed calls to 'clear_inode' (function is undefined)
Removed calls to 'obd_zombie_barrier' (function is undefined)
Removed calls to 'class_del_profile' (function is undefined)
Removed calls to 'bdi_destroy' (function is undefined)
Removed calls to 'module_put' (function is undefined)
Removed calls to 'statfs_unpack' (function is undefined)
Defining function seq_puts as symbolic
Defining function lustre_end_log as symbolic
Defining function class_devices_in_group as symbolic
Defining function class_manual_cleanup as symbolic
Defining function lustre_common_put_super as symbolic
Removed calls to 'wait_for_completion' (function is undefined)
Removed calls to 'cl_stack_fini' (function is undefined)
Removed calls to 'lu_types_stop' (function is undefined)
Removed calls to 'ldebugfs_remove' (function is undefined)
Removed calls to 'kobject_put' (function is undefined)
Removed calls to 'lprocfs_free_stats' (function is undefined)
Removed calls to 'cl_object_kill' (function is undefined)
Removed calls to 'cfs_hash_bd_get' (function is undefined)
Removed calls to 'cl_object_put' (function is undefined)
Removed calls to 'cl_env_reexit' (function is undefined)
Defining function cl_env_reenter as symbolic
Defining function seq_lseek as symbolic
Defining function seq_read as symbolic
Defining function seq_release as symbolic
Defining function seq_open as symbolic
Removed calls to 'cl_site_fini' (function is undefined)
Removed calls to 'lu_device_fini' (function is undefined)
Removed calls to 'lu_device_get' (function is undefined)
Removed calls to 'ldv__builtin_va_start' (function is undefined)
Removed calls to 'ldv__builtin_va_arg' (function is undefined)
Removed calls to 'ldv__builtin_va_end' (function is undefined)
Removed calls to 'lu_context_key_degister_many' (function is undefined)
Removed calls to 'lu_context_key_revive_many' (function is undefined)
Removed calls to 'lu_context_key_quiesce_many' (function is undefined)
Defining function lu_context_key_register_many as symbolic
Defining function cl_site_init as symbolic
Defining function lu_site_init_finish as symbolic
Defining function lu_device_init as symbolic
Removed calls to 'cfs_hash_hlist_for_each' (function is undefined)
Removed calls to 'lu_object_put' (function is undefined)
Defining function cl_page_lookup as symbolic
Defining function seq_printf as symbolic
Defining function cl_page_at as symbolic
Removed calls to 'lu_object_add_top' (function is undefined)
Defining function cl_object_header_init as symbolic
Defining function lu_object_init as symbolic
Removed calls to 'cl_req_slice_add' (function is undefined)
Removed calls to 'cl_page_header_print' (function is undefined)
Removed calls to 'cl_page_export' (function is undefined)
Removed calls to 'end_page_writeback' (function is undefined)
Removed calls to 'cl_page_print' (function is undefined)
Defining function clear_page_dirty_for_io as symbolic
Defining function lu_cdebug_printer as symbolic
Defining function __test_set_page_writeback as symbolic
Removed calls to 'free_pages' (function is undefined)
Defining function d_find_alias as symbolic
Defining function dentry_path_raw as symbolic
Defining function cl_page_top as symbolic
Defining function cl_queue_match as symbolic
Removed calls to 'unmap_mapping_range' (function is undefined)
Removed calls to 'lu_object_header_print' (function is undefined)
Removed calls to 'touch_atime' (function is undefined)
Removed calls to 'truncate_setsize' (function is undefined)
Removed calls to 'cl_page_discard' (function is undefined)
Defining function cl_page_is_vmlocked as symbolic
Defining function cl_page_cache_add as symbolic
Removed calls to 'cl_2queue_init_page' (function is undefined)
Removed calls to 'cl_page_list_disown' (function is undefined)
Defining function cl_page_is_under_lock as symbolic
Removed calls to 'cl_page_list_add' (function is undefined)
Defining function pagecache_get_page as symbolic
Defining function cl_page_unmap as symbolic
Defining function filemap_fault as symbolic
Defining function cl_io_lock_add as symbolic
Defining function cl_object_attr_set as symbolic
Defining function generic_file_write_iter as symbolic
Removed calls to 'lprocfs_oh_clear' (function is undefined)
Defining function cl_io_lock_alloc_add as symbolic
Defining function find_vma as symbolic
Defining function generic_file_read_iter as symbolic
Defining function generic_file_splice_read as symbolic
Removed calls to 'cl_page_slice_add' (function is undefined)
Removed calls to 'cl_io_slice_add' (function is undefined)
Defining function lustre_get_jobid as symbolic
Removed calls to 'cl_lock_slice_add' (function is undefined)
Removed calls to 'lu_object_add' (function is undefined)
Removed calls to 'lu_object_fini' (function is undefined)
Removed calls to 'lu_object_header_fini' (function is undefined)
Defining function lprocfs_single_release as symbolic
Defining function single_open as symbolic
Defining function cl_site_stats_print as symbolic
Defining function lprocfs_find_named_value as symbolic
Defining function lprocfs_write_frac_helper as symbolic
Removed calls to 'complete' (function is undefined)
Defining function kstrtoull as symbolic
Defining function lprocfs_read_frac_helper as symbolic
Removed calls to 'lprocfs_clear_stats' (function is undefined)
Removed calls to 'do_gettimeofday' (function is undefined)
Defining function lprocfs_write_helper as symbolic
Removed calls to 'add_wait_queue_exclusive' (function is undefined)
Removed calls to 'si_meminfo' (function is undefined)
Removed calls to 'cfs_get_random_bytes' (function is undefined)
Removed calls to 'class_uuid_unparse' (function is undefined)
Defining function try_module_get as symbolic
Defining function bdi_init as symbolic
Defining function class_config_llog_handler as symbolic
Defining function lustre_process_log as symbolic
Defining function class_get_profile as symbolic
Defining function kasprintf as symbolic
Defining function class_name2obd as symbolic
Removed calls to 'lprocfs_counter_init' (function is undefined)
Defining function obd_connect_flags2str as symbolic
Defining function d_make_root as symbolic
Defining function cl_type_setup as symbolic
Defining function cfs_crypto_hash_speed as symbolic
Defining function snprintf as symbolic
Defining function ldebugfs_register as symbolic
Defining function ldebugfs_seq_create as symbolic
Defining function lprocfs_alloc_stats as symbolic
Defining function ldebugfs_register_stats as symbolic
Defining function ldebugfs_add_vars as symbolic
Defining function kobject_init_and_add as symbolic
Defining function sysfs_create_link as symbolic
Defining function bdi_register as symbolic
Defining function class_process_proc_param as symbolic
Defining function ldv_release_51 as symbolic
Defining function ldv_probe_51 as symbolic
Defining function lu_kmem_init as symbolic
Removed calls to 'lu_kmem_fini' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Defining function prepare_to_wait_event as symbolic
Defining function ldv_release_49 as symbolic
Defining function ldv_probe_49 as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'lustre_register_client_fill_super' (function is undefined)
Removed calls to 'lustre_register_kill_super_cb' (function is undefined)
Removed calls to 'lustre_register_client_process_config' (function is undefined)
Removed calls to 'debugfs_remove' (function is undefined)
Removed calls to 'kset_unregister' (function is undefined)
Removed calls to 'kmem_cache_destroy' (function is undefined)
Removed calls to 'cfs_srand' (function is undefined)
Removed calls to 'ldv_check_final_state' (function is undefined)
Defining function ldv_probe_5 as symbolic
Defining function ldv_release_34 as symbolic
Defining function ldv_probe_34 as symbolic
Defining function kmem_cache_create as symbolic
Defining function debugfs_create_dir as symbolic
Defining function kset_create_and_add as symbolic
Defining function LNetGetId as symbolic
Defining function del_timer as symbolic
Removed calls to 'lu_device_type_fini' (function is undefined)
Defining function lu_device_type_init as symbolic
Defining function cl_env_alloc as symbolic
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  memchr
  memcmp
  strchr
  strcmp
  strlen
  strncmp
  strncpy
  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: 4.86618208885
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 2230 1225 9446 92889
INFO: Starting verification
KLEE: WARNING ONCE: function "ll_dir_ioctl" has inline asm
KLEE: WARNING ONCE: function "ll_stats_ops_tally" has inline asm
KLEE: WARNING ONCE: function "ll_mdscapa_get" has inline asm
KLEE: WARNING ONCE: function "capa_put" has inline asm
KLEE: WARNING ONCE: function "ll_osscapa_get" has inline asm
KLEE: WARNING ONCE: function "ll_file_release" has inline asm
KLEE: WARNING ONCE: function "ll_stop_statahead" has inline asm
KLEE: WARNING ONCE: function "ll_prep_md_op_data" has inline asm
KLEE: WARNING ONCE: function "ll_som_update" has inline asm
KLEE: WARNING ONCE: function "ll_objects_destroy" has inline asm
KLEE: WARNING ONCE: function "cl_local_size" has inline asm
KLEE: WARNING ONCE: function "cl_put_grouplock" has inline asm
KLEE: WARNING ONCE: function "ll_sa_entry_put" has inline asm
KLEE: WARNING ONCE: function "ll_file_open" has inline asm
KLEE: WARNING ONCE: function "posix_acl_release" has inline asm
KLEE: WARNING ONCE: function "ll_update_remote_perm" has inline asm
KLEE: WARNING ONCE: function "ll_iocontrol" has inline asm
KLEE: WARNING ONCE: function "ll_flush_ctx" has inline asm
KLEE: WARNING ONCE: function "ll_fid2path" has inline asm
KLEE: WARNING ONCE: function "ll_need_32bit_api" has inline asm
KLEE: WARNING ONCE: function "ll_get_dir_page" has inline asm
KLEE: WARNING ONCE: function "lock_page" has inline asm
KLEE: WARNING ONCE: function "truncate_complete_page" has inline asm
KLEE: WARNING ONCE: function "ll_dir_filler" has inline asm
KLEE: WARNING ONCE: function "ll_file_ioctl" has inline asm
KLEE: WARNING ONCE: function "ll_vm_open" has inline asm
KLEE: WARNING ONCE: function "cl_glimpse_lock" has inline asm
KLEE: WARNING ONCE: function "ll_lov_recreate" has inline asm
KLEE: WARNING ONCE: function "ll_setattr_raw" has inline asm
KLEE: WARNING ONCE: function "cl_get_grouplock" has inline asm
KLEE: WARNING ONCE: function "ll_get_acl" has inline asm
KLEE: WARNING ONCE: function "ll_setxattr_common" has inline asm
KLEE: WARNING ONCE: function "ll_getxattr_common" has inline asm
KLEE: WARNING ONCE: function "ll_xattr_cache_get" has inline asm
KLEE: WARNING ONCE: function "do_check_remote_perm" has inline asm
KLEE: WARNING ONCE: function "d_need_statahead" has inline asm
KLEE: WARNING ONCE: function "do_statahead_enter" has inline asm
KLEE: WARNING ONCE: function "ll_statahead_mark" has inline asm
KLEE: WARNING ONCE: function "ll_sai_unplug" has inline asm
KLEE: WARNING ONCE: function "ll_statahead_thread" has inline asm
KLEE: WARNING ONCE: function "ll_agl_thread" has inline asm
KLEE: WARNING ONCE: function "ll_post_statahead" has inline asm
KLEE: WARNING ONCE: function "ll_statahead_interpret" has inline asm
KLEE: WARNING ONCE: function "ll_new_node" has inline asm
KLEE: WARNING ONCE: function "ll_direct_rw_pages" has inline asm
KLEE: WARNING ONCE: function "__kunmap_atomic" has inline asm
KLEE: WARNING ONCE: function "ll_writepage" has inline asm
KLEE: WARNING ONCE: function "ll_commit_write" has inline asm
KLEE: WARNING ONCE: function "ll_cl_fini" has inline asm
KLEE: WARNING ONCE: function "ll_cl_init" has inline asm
KLEE: WARNING ONCE: function "ll_alloc_inode" has inline asm
KLEE: WARNING ONCE: function "ll_close_thread_shutdown" has inline asm
KLEE: WARNING ONCE: function "cl_inode_fini" has inline asm
KLEE: WARNING ONCE: function "ccc_key_init" has inline asm
KLEE: WARNING ONCE: function "ccc_session_key_init" has inline asm
KLEE: WARNING ONCE: function "vvp_key_init" has inline asm
KLEE: WARNING ONCE: function "vvp_session_key_init" has inline asm
KLEE: WARNING ONCE: function "ll_vm_close" has inline asm
KLEE: WARNING ONCE: function "ll_fault" has inline asm
KLEE: WARNING ONCE: function "ll_page_mkwrite" has inline asm
KLEE: WARNING ONCE: function "ccc_object_alloc" has inline asm
KLEE: WARNING ONCE: function "ccc_req_init" has inline asm
KLEE: WARNING ONCE: function "vvp_page_own" has inline asm
KLEE: WARNING ONCE: function "vvp_page_export" has inline asm
KLEE: WARNING ONCE: function "vvp_page_delete" has inline asm
KLEE: WARNING ONCE: function "vvp_page_print" has inline asm
KLEE: WARNING ONCE: function "vvp_page_completion_read" has inline asm
KLEE: WARNING ONCE: function "vvp_page_completion_write" has inline asm
KLEE: WARNING ONCE: function "vvp_io_read_start" has inline asm
KLEE: WARNING ONCE: function "vvp_io_write_start" has inline asm
KLEE: WARNING ONCE: function "vvp_io_prepare_write" has inline asm
KLEE: WARNING ONCE: function "ll_readahead" has inline asm
KLEE: WARNING ONCE: function "vvp_io_rw_lock" has inline asm
KLEE: WARNING ONCE: function "ll_ra_read_in" has inline asm
KLEE: WARNING ONCE: function "vvp_page_init" has inline asm
KLEE: WARNING ONCE: function "ccc_lock_init" has inline asm
KLEE: WARNING ONCE: function "ll_max_cached_mb_seq_write" has inline asm
KLEE: WARNING ONCE: function "ll_capa_close" has inline asm
KLEE: WARNING ONCE: function "ll_capa_open" has inline asm
KLEE: WARNING ONCE: function "ll_ra_count_put" has inline asm
KLEE: WARNING ONCE: function "ll_close_thread" has inline asm
KLEE: WARNING ONCE: function "ll_fill_super" has inline asm
KLEE: WARNING ONCE: function "ll_ra_read_get" has inline asm
KLEE: WARNING ONCE: function "capa_thread_main" has inline asm
KLEE: WARNING: undefined reference to variable: RMF_ACL
KLEE: WARNING: undefined reference to variable: RMF_CAPA2
KLEE: WARNING: undefined reference to variable: RMF_EADATA
KLEE: WARNING: undefined reference to variable: RMF_EAVALS
KLEE: WARNING: undefined reference to variable: RMF_EAVALS_LENS
KLEE: WARNING: undefined reference to variable: RMF_LOGCOOKIES
KLEE: WARNING: undefined reference to variable: RMF_MDT_BODY
KLEE: WARNING: undefined reference to variable: RMF_MDT_MD
KLEE: WARNING: undefined reference to variable: capa_cachep
KLEE: WARNING: undefined reference to variable: init_user_ns
KLEE: WARNING: undefined reference to function: lustre_swab_mdt_remote_perm
KLEE: WARNING: undefined reference to variable: obdo_cachep
KLEE: ERROR: unable to load symbol(capa_cachep) while initializing globals.
KLEE: output directory is "/tmp/symbiotic-JfJJyS/klee-out-0"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: function "ll_dir_ioctl" has inline asm
KLEE: WARNING ONCE: function "ll_stats_ops_tally" has inline asm
KLEE: WARNING ONCE: function "ll_mdscapa_get" has inline asm
KLEE: WARNING ONCE: function "capa_put" has inline asm
KLEE: WARNING ONCE: function "ll_osscapa_get" has inline asm
KLEE: WARNING ONCE: function "ll_file_release" has inline asm
KLEE: WARNING ONCE: function "ll_stop_statahead" has inline asm
KLEE: WARNING ONCE: function "ll_prep_md_op_data" has inline asm
KLEE: WARNING ONCE: function "ll_som_update" has inline asm
KLEE: WARNING ONCE: function "ll_objects_destroy" has inline asm
KLEE: WARNING ONCE: function "cl_local_size" has inline asm
KLEE: WARNING ONCE: function "cl_put_grouplock" has inline asm
KLEE: WARNING ONCE: function "ll_sa_entry_put" has inline asm
KLEE: WARNING ONCE: function "ll_file_open" has inline asm
KLEE: WARNING ONCE: function "posix_acl_release" has inline asm
KLEE: WARNING ONCE: function "ll_update_remote_perm" has inline asm
KLEE: WARNING ONCE: function "ll_iocontrol" has inline asm
KLEE: WARNING ONCE: function "ll_flush_ctx" has inline asm
KLEE: WARNING ONCE: function "ll_fid2path" has inline asm
KLEE: WARNING ONCE: function "ll_need_32bit_api" has inline asm
KLEE: WARNING ONCE: function "ll_get_dir_page" has inline asm
KLEE: WARNING ONCE: function "lock_page" has inline asm
KLEE: WARNING ONCE: function "truncate_complete_page" has inline asm
KLEE: WARNING ONCE: function "ll_dir_filler" has inline asm
KLEE: WARNING ONCE: function "ll_file_ioctl" has inline asm
KLEE: WARNING ONCE: function "ll_vm_open" has inline asm
KLEE: WARNING ONCE: function "cl_glimpse_lock" has inline asm
KLEE: WARNING ONCE: function "ll_lov_recreate" has inline asm
KLEE: WARNING ONCE: function "ll_setattr_raw" has inline asm
KLEE: WARNING ONCE: function "cl_get_grouplock" has inline asm
KLEE: WARNING ONCE: function "ll_get_acl" has inline asm
KLEE: WARNING ONCE: function "ll_setxattr_common" has inline asm
KLEE: WARNING ONCE: function "ll_getxattr_common" has inline asm
KLEE: WARNING ONCE: function "ll_xattr_cache_get" has inline asm
KLEE: WARNING ONCE: function "do_check_remote_perm" has inline asm
KLEE: WARNING ONCE: function "d_need_statahead" has inline asm
KLEE: WARNING ONCE: function "do_statahead_enter" has inline asm
KLEE: WARNING ONCE: function "ll_statahead_mark" has inline asm
KLEE: WARNING ONCE: function "ll_sai_unplug" has inline asm
KLEE: WARNING ONCE: function "ll_statahead_thread" has inline asm
KLEE: WARNING ONCE: function "ll_agl_thread" has inline asm
KLEE: WARNING ONCE: function "ll_post_statahead" has inline asm
KLEE: WARNING ONCE: function "ll_statahead_interpret" has inline asm
KLEE: WARNING ONCE: function "ll_new_node" has inline asm
KLEE: WARNING ONCE: function "ll_direct_rw_pages" has inline asm
KLEE: WARNING ONCE: function "__kunmap_atomic" has inline asm
KLEE: WARNING ONCE: function "ll_writepage" has inline asm
KLEE: WARNING ONCE: function "ll_commit_write" has inline asm
KLEE: WARNING ONCE: function "ll_cl_fini" has inline asm
KLEE: WARNING ONCE: function "ll_cl_init" has inline asm
KLEE: WARNING ONCE: function "ll_alloc_inode" has inline asm
KLEE: WARNING ONCE: function "ll_close_thread_shutdown" has inline asm
KLEE: WARNING ONCE: function "cl_inode_fini" has inline asm
KLEE: WARNING ONCE: function "ccc_key_init" has inline asm
KLEE: WARNING ONCE: function "ccc_session_key_init" has inline asm
KLEE: WARNING ONCE: function "vvp_key_init" has inline asm
KLEE: WARNING ONCE: function "vvp_session_key_init" has inline asm
KLEE: WARNING ONCE: function "ll_vm_close" has inline asm
KLEE: WARNING ONCE: function "ll_fault" has inline asm
KLEE: WARNING ONCE: function "ll_page_mkwrite" has inline asm
KLEE: WARNING ONCE: function "ccc_object_alloc" has inline asm
KLEE: WARNING ONCE: function "ccc_req_init" has inline asm
KLEE: WARNING ONCE: function "vvp_page_own" has inline asm
KLEE: WARNING ONCE: function "vvp_page_export" has inline asm
KLEE: WARNING ONCE: function "vvp_page_delete" has inline asm
KLEE: WARNING ONCE: function "vvp_page_print" has inline asm
KLEE: WARNING ONCE: function "vvp_page_completion_read" has inline asm
KLEE: WARNING ONCE: function "vvp_page_completion_write" has inline asm
KLEE: WARNING ONCE: function "vvp_io_read_start" has inline asm
KLEE: WARNING ONCE: function "vvp_io_write_start" has inline asm
KLEE: WARNING ONCE: function "vvp_io_prepare_write" has inline asm
KLEE: WARNING ONCE: function "ll_readahead" has inline asm
KLEE: WARNING ONCE: function "vvp_io_rw_lock" has inline asm
KLEE: WARNING ONCE: function "ll_ra_read_in" has inline asm
KLEE: WARNING ONCE: function "vvp_page_init" has inline asm
KLEE: WARNING ONCE: function "ccc_lock_init" has inline asm
KLEE: WARNING ONCE: function "ll_max_cached_mb_seq_write" has inline asm
KLEE: WARNING ONCE: function "ll_capa_close" has inline asm
KLEE: WARNING ONCE: function "ll_capa_open" has inline asm
KLEE: WARNING ONCE: function "ll_ra_count_put" has inline asm
KLEE: WARNING ONCE: function "ll_close_thread" has inline asm
KLEE: WARNING ONCE: function "ll_fill_super" has inline asm
KLEE: WARNING ONCE: function "ll_ra_read_get" has inline asm
KLEE: WARNING ONCE: function "capa_thread_main" has inline asm
KLEE: WARNING: undefined reference to variable: RMF_ACL
KLEE: WARNING: undefined reference to variable: RMF_CAPA2
KLEE: WARNING: undefined reference to variable: RMF_EADATA
KLEE: WARNING: undefined reference to variable: RMF_EAVALS
KLEE: WARNING: undefined reference to variable: RMF_EAVALS_LENS
KLEE: WARNING: undefined reference to variable: RMF_LOGCOOKIES
KLEE: WARNING: undefined reference to variable: RMF_MDT_BODY
KLEE: WARNING: undefined reference to variable: RMF_MDT_MD
KLEE: WARNING: undefined reference to variable: capa_cachep
KLEE: WARNING: undefined reference to variable: init_user_ns
KLEE: WARNING: undefined reference to function: lustre_swab_mdt_remote_perm
KLEE: WARNING: undefined reference to variable: obdo_cachep
KLEE: ERROR: unable to load symbol(capa_cachep) while initializing globals.
Running the verifier failed
RESULT: unknown
INFO: Total time elapsed: 10.74716115
