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-32_7a-drivers--staging--lustre--lustre--mdc--mdc.ko-entry_point_false-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.: 522 410 4313 31221
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 1.25071907043
Removed calls to 'lbug_with_loc' (function is undefined)
Defining function libcfs_debug_msg as symbolic
Removed calls to 'lprocfs_counter_add' (function is undefined)
Removed calls to 'ptlrpc_request_set_replen' (function is undefined)
Removed calls to 'ptlrpc_req_finished' (function is undefined)
Removed calls to 'req_capsule_set_size' (function is undefined)
Removed calls to 'ptlrpc_request_free' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to 'ldlm_lock_put' (function is undefined)
Removed calls to 'module_put' (function is undefined)
Removed calls to 'lustre_swab_fid2path' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'sptlrpc_conf_client_adapt' (function is undefined)
Removed calls to 'sptlrpc_import_flush_my_ctx' (function is undefined)
Removed calls to 'lustre_swab_lu_fid' (function is undefined)
Removed calls to 'ptlrpc_lprocfs_register_obd' (function is undefined)
Removed calls to 'ptlrpcd_decref' (function is undefined)
Removed calls to 'down_write' (function is undefined)
Removed calls to 'ptlrpc_invalidate_import' (function is undefined)
Removed calls to 'ptlrpc_free_rq_pool' (function is undefined)
Removed calls to 'client_destroy_import' (function is undefined)
Removed calls to 'up_write' (function is undefined)
Removed calls to 'ptlrpc_lprocfs_unregister_obd' (function is undefined)
Defining function client_import_add_conn as symbolic
Defining function client_import_del_conn as symbolic
Defining function client_connect_import as symbolic
Defining function client_disconnect_export as symbolic
Defining function client_fid_init as symbolic
Defining function client_fid_fini as symbolic
Removed calls to 'down_read' (function is undefined)
Removed calls to 'up_read' (function is undefined)
Removed calls to 'class_import_put' (function is undefined)
Removed calls to 'seq_client_flush' (function is undefined)
Removed calls to 'ptlrpc_at_set_req_timeout' (function is undefined)
Defining function class_exp2cliimp as symbolic
Defining function ptlrpc_request_alloc_pack as symbolic
Defining function req_capsule_client_get as symbolic
Defining function ptlrpc_queue_wait as symbolic
Defining function req_capsule_server_get as symbolic
Defining function ldlm_namespace_cleanup as symbolic
Defining function libcfs_kkuc_group_foreach as symbolic
Removed calls to '__list_add' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'add_wait_queue' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'cfs_restore_sigs' (function is undefined)
Removed calls to 'remove_wait_queue' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Removed calls to 'dump_stack' (function is undefined)
Defining function schedule_timeout as symbolic
Defining function _raw_spin_trylock as symbolic
Defining function cfs_block_sigsinv as symbolic
Defining function cfs_signal_pending as symbolic
Defining function default_wake_function as symbolic
Removed calls to 'capa_cpy' (function is undefined)
Removed calls to '_debug_capa' (function is undefined)
Defining function req_capsule_get_size as symbolic
Defining function debug_lockdep_rcu_enabled as symbolic
Defining function from_kuid as symbolic
Defining function from_kgid as symbolic
Defining function cfs_curproc_cap_pack as symbolic
Defining function class_exp2obd as symbolic
Defining function class_import_get as symbolic
Defining function seq_client_alloc_fid as symbolic
Defining function class_process_proc_param as symbolic
Defining function client_obd_cleanup as symbolic
Defining function libcfs_kkuc_group_rem as symbolic
Defining function lprocfs_obd_cleanup as symbolic
Defining function llog_cleanup as symbolic
Removed calls to '__mutex_init' (function is undefined)
Defining function ptlrpcd_addref as symbolic
Defining function client_obd_setup as symbolic
Defining function lprocfs_obd_setup as symbolic
Defining function sptlrpc_lprocfs_cliobd_attach as symbolic
Defining function llog_setup as symbolic
Defining function llog_initiator_connect as symbolic
Defining function __llog_ctxt_put as symbolic
Defining function do_set_info_async as symbolic
Defining function libcfs_kkuc_group_put as symbolic
Defining function ptlrpc_request_alloc as symbolic
Defining function ptlrpc_request_pack as symbolic
Defining function try_module_get as symbolic
Defining function ptlrpc_recover_import as symbolic
Defining function ptlrpc_set_import_active as symbolic
Defining function ptlrpc_obd_ping as symbolic
Removed calls to '__might_fault' (function is undefined)
Removed calls to '__copy_to_user_overflow' (function is undefined)
Defining function ldlm_prep_elc_req as symbolic
Defining function ldlm_resource_get as symbolic
Defining function ldlm_cancel_resource_local as symbolic
Defining function ldlm_resource_putref as symbolic
Defining function _copy_to_user as symbolic
Defining function fget as symbolic
Removed calls to 'fput' (function is undefined)
Defining function kthread_create_on_node as symbolic
Defining function wake_up_process as symbolic
Defining function llog_open as symbolic
Defining function llog_init_handle as symbolic
Defining function llog_cat_process as symbolic
Defining function libcfs_kkuc_msg_put as symbolic
Defining function llog_cat_close as symbolic
Removed calls to 'lustre_msg_add_flags' (function is undefined)
Removed calls to '_debug_req' (function is undefined)
Removed calls to 'lprocfs_counter_sub' (function is undefined)
Removed calls to 'ldlm_lock_decref' (function is undefined)
Removed calls to '__ptlrpc_prep_bulk_page' (function is undefined)
Removed calls to 'cfs_clear_sigpending' (function is undefined)
Removed calls to 'unlock_res_and_lock' (function is undefined)
Removed calls to 'ptlrpcd_add_req' (function is undefined)
Removed calls to 'kmem_cache_free' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Defining function ldlm_revalidate_lock_handle as symbolic
Defining function ldlm_it2str as symbolic
Defining function ldlm_cli_enqueue as symbolic
Defining function ldlm_cli_enqueue_fini as symbolic
Removed calls to 'ldlm_lock_addref' (function is undefined)
Removed calls to 'req_capsule_shrink' (function is undefined)
Removed calls to '_ldlm_lock_debug' (function is undefined)
Removed calls to 'kvfree' (function is undefined)
Removed calls to 'ldlm_lock_decref_and_cancel' (function is undefined)
Defining function ptlrpc_request_addref as symbolic
Defining function ldlm_lock_match as symbolic
Defining function __ldlm_handle2lock as symbolic
Defining function __cfs_fail_timeout_set as symbolic
Defining function req_capsule_server_sized_get as symbolic
Defining function req_capsule_server_swab_get as symbolic
Defining function libcfs_kvzalloc as symbolic
Defining function lock_res_and_lock as symbolic
Defining function sptlrpc_cli_enlarge_reqbuf as symbolic
Defining function __cfs_fail_check_set as symbolic
Defining function ldlm_prep_enqueue_req as symbolic
Defining function kmem_cache_alloc as symbolic
Defining function obd_alloc_fail as symbolic
Defining function ldlm_cli_cancel_unused_resource as symbolic
Removed calls to 'ptlrpc_request_committed' (function is undefined)
Defining function lustre_msg_get_opc as symbolic
Removed calls to 'kfree_call_rcu' (function is undefined)
Defining function posix_acl_from_xattr as symbolic
Defining function posix_acl_valid as symbolic
Defining function get_seconds as symbolic
Defining function req_capsule_has_field as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function ptlrpc_prep_bulk_imp as symbolic
Defining function sptlrpc_cli_unwrap_bulk_read as symbolic
Defining function in_group_p as symbolic
Defining function ldlm_cli_cancel_list as symbolic
Defining function ldlm_completion_ast as symbolic
Defining function strnlen as symbolic
Defining function current_umask as symbolic
Defining function ldlm_cli_cancel as symbolic
Defining function lustre_msg_get_status as symbolic
Defining function lustre_msg_get_type as symbolic
Defining function ldlm_resource_iterate as symbolic
Defining function lustre_msg_get_last_committed as symbolic
Defining function kstrtoull as symbolic
Defining function sprintf as symbolic
Defining function lprocfs_single_release as symbolic
Defining function single_open as symbolic
Defining function lprocfs_wr_ping as symbolic
Defining function seq_lseek as symbolic
Defining function seq_read as symbolic
Defining function lprocfs_rd_connect_flags as symbolic
Defining function lprocfs_rd_server_uuid as symbolic
Defining function lprocfs_rd_conn_uuid as symbolic
Defining function lprocfs_rd_timeouts as symbolic
Defining function lprocfs_rd_import as symbolic
Defining function lprocfs_wr_import as symbolic
Defining function lprocfs_rd_state as symbolic
Defining function single_release as symbolic
Defining function lprocfs_write_helper as symbolic
Defining function lprocfs_rd_pinger_recov as symbolic
Defining function lprocfs_wr_pinger_recov as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Defining function ldv_release_12 as symbolic
Defining function ldv_probe_12 as symbolic
Defining function ldv_probe_13 as symbolic
Defining function class_register_type as symbolic
Defining function class_unregister_type as symbolic
Defining function mutex_trylock as symbolic
Linked our definitions to these undefined functions:
  memcmp
  strlen
  strncpy
  strrchr
  __kmalloc
  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: 1.06817507744
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 671 408 2461 20451
INFO: Starting verification
KLEE: WARNING ONCE: function "mdc_enter_request" has inline asm
KLEE: WARNING ONCE: function "__client_obd_list_lock" has inline asm
KLEE: WARNING ONCE: function "__mdc_pack_body" has inline asm
KLEE: WARNING ONCE: function "llog_group_get_ctxt" has inline asm
KLEE: WARNING ONCE: function "mdc_close" has inline asm
KLEE: WARNING ONCE: function "mdc_done_writing" has inline asm
KLEE: WARNING ONCE: function "mdc_setattr" has inline asm
KLEE: WARNING ONCE: function "mdc_readpage" has inline asm
KLEE: WARNING ONCE: function "mdc_set_open_replay_data" has inline asm
KLEE: WARNING ONCE: function "mdc_clear_open_replay_data" has inline asm
KLEE: WARNING ONCE: function "mdc_unpack_capa" has inline asm
KLEE: WARNING ONCE: function "mdc_commit_open" has inline asm
KLEE: WARNING ONCE: function "posix_acl_release" has inline asm
KLEE: WARNING ONCE: function "capa_put" has inline asm
KLEE: WARNING ONCE: function "mdc_xattr_common" has inline asm
KLEE: WARNING ONCE: function "mdc_setattr_pack_rec" has inline asm
KLEE: WARNING ONCE: function "mdc_open_pack" has inline asm
KLEE: WARNING ONCE: function "__client_obd_list_lock___0" has inline asm
KLEE: WARNING: undefined reference to variable: RMF_ACL
KLEE: WARNING: undefined reference to variable: RMF_CAPA1
KLEE: WARNING: undefined reference to variable: RMF_CAPA2
KLEE: WARNING: undefined reference to variable: RMF_CLOSE_DATA
KLEE: WARNING: undefined reference to variable: RMF_DLM_LVB
KLEE: WARNING: undefined reference to variable: RMF_DLM_REP
KLEE: WARNING: undefined reference to variable: RMF_DLM_REQ
KLEE: WARNING: undefined reference to variable: RMF_EADATA
KLEE: WARNING: undefined reference to variable: RMF_GENERIC_DATA
KLEE: WARNING: undefined reference to variable: RMF_GETINFO_KEY
KLEE: WARNING: undefined reference to variable: RMF_GETINFO_VAL
KLEE: WARNING: undefined reference to variable: RMF_GETINFO_VALLEN
KLEE: WARNING: undefined reference to variable: RMF_HSM_STATE_SET
KLEE: WARNING: undefined reference to variable: RMF_HSM_USER_STATE
KLEE: WARNING: undefined reference to variable: RMF_LAYOUT_INTENT
KLEE: WARNING: undefined reference to variable: RMF_LDLM_INTENT
KLEE: WARNING: undefined reference to variable: RMF_LOGCOOKIES
KLEE: WARNING: undefined reference to variable: RMF_MDS_HSM_ARCHIVE
KLEE: WARNING: undefined reference to variable: RMF_MDS_HSM_CURRENT_ACTION
KLEE: WARNING: undefined reference to variable: RMF_MDS_HSM_PROGRESS
KLEE: WARNING: undefined reference to variable: RMF_MDS_HSM_REQUEST
KLEE: WARNING: undefined reference to variable: RMF_MDS_HSM_USER_ITEM
KLEE: WARNING: undefined reference to variable: RMF_MDT_BODY
KLEE: WARNING: undefined reference to variable: RMF_MDT_EPOCH
KLEE: WARNING: undefined reference to variable: RMF_MDT_MD
KLEE: WARNING: undefined reference to variable: RMF_NAME
KLEE: WARNING: undefined reference to variable: RMF_OBD_QUOTACTL
KLEE: WARNING: undefined reference to variable: RMF_OBD_STATFS
KLEE: WARNING: undefined reference to variable: RMF_REC_REINT
KLEE: WARNING: undefined reference to variable: RMF_SWAP_LAYOUTS
KLEE: WARNING: undefined reference to variable: RMF_SYMTGT
KLEE: WARNING: undefined reference to variable: RQF_LDLM_ENQUEUE
KLEE: WARNING: undefined reference to variable: RQF_LDLM_INTENT_GETATTR
KLEE: WARNING: undefined reference to variable: RQF_LDLM_INTENT_GETXATTR
KLEE: WARNING: undefined reference to variable: RQF_LDLM_INTENT_LAYOUT
KLEE: WARNING: undefined reference to variable: RQF_LDLM_INTENT_OPEN
KLEE: WARNING: undefined reference to variable: RQF_LDLM_INTENT_UNLINK
KLEE: WARNING: undefined reference to variable: RQF_MDS_CLOSE
KLEE: WARNING: undefined reference to variable: RQF_MDS_DONE_WRITING
KLEE: WARNING: undefined reference to variable: RQF_MDS_GETATTR
KLEE: WARNING: undefined reference to variable: RQF_MDS_GETATTR_NAME
KLEE: WARNING: undefined reference to variable: RQF_MDS_GETSTATUS
KLEE: WARNING: undefined reference to variable: RQF_MDS_GETXATTR
KLEE: WARNING: undefined reference to variable: RQF_MDS_GET_INFO
KLEE: WARNING: undefined reference to variable: RQF_MDS_HSM_ACTION
KLEE: WARNING: undefined reference to variable: RQF_MDS_HSM_CT_REGISTER
KLEE: WARNING: undefined reference to variable: RQF_MDS_HSM_CT_UNREGISTER
KLEE: WARNING: undefined reference to variable: RQF_MDS_HSM_PROGRESS
KLEE: WARNING: undefined reference to variable: RQF_MDS_HSM_REQUEST
KLEE: WARNING: undefined reference to variable: RQF_MDS_HSM_STATE_GET
KLEE: WARNING: undefined reference to variable: RQF_MDS_HSM_STATE_SET
KLEE: WARNING: undefined reference to variable: RQF_MDS_IS_SUBDIR
KLEE: WARNING: undefined reference to variable: RQF_MDS_QUOTACHECK
KLEE: WARNING: undefined reference to variable: RQF_MDS_QUOTACTL
KLEE: WARNING: undefined reference to variable: RQF_MDS_READPAGE
KLEE: WARNING: undefined reference to variable: RQF_MDS_REINT_CREATE_RMT_ACL
KLEE: WARNING: undefined reference to variable: RQF_MDS_REINT_LINK
KLEE: WARNING: undefined reference to variable: RQF_MDS_REINT_RENAME
KLEE: WARNING: undefined reference to variable: RQF_MDS_REINT_SETATTR
KLEE: WARNING: undefined reference to variable: RQF_MDS_REINT_SETXATTR
KLEE: WARNING: undefined reference to variable: RQF_MDS_REINT_UNLINK
KLEE: WARNING: undefined reference to variable: RQF_MDS_RELEASE_CLOSE
KLEE: WARNING: undefined reference to variable: RQF_MDS_STATFS
KLEE: WARNING: undefined reference to variable: RQF_MDS_SWAP_LAYOUTS
KLEE: WARNING: undefined reference to variable: RQF_MDS_SYNC
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: Type for RQF_MDS_QUOTACTL is not sized
KLEE: WARNING: Unable to find size for global variable: RQF_MDS_QUOTACTL (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_OBD_QUOTACTL is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_OBD_QUOTACTL (use will result in out of bounds access)
KLEE: WARNING: Type for RQF_MDS_QUOTACHECK is not sized
KLEE: WARNING: Unable to find size for global variable: RQF_MDS_QUOTACHECK (use will result in out of bounds access)
KLEE: WARNING: Type for RQF_MDS_HSM_CT_REGISTER is not sized
KLEE: WARNING: Unable to find size for global variable: RQF_MDS_HSM_CT_REGISTER (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_MDS_HSM_ARCHIVE is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_MDS_HSM_ARCHIVE (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_MDT_BODY is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_MDT_BODY (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_CAPA1 is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_CAPA1 (use will result in out of bounds access)
KLEE: WARNING: Type for init_user_ns is not sized
KLEE: WARNING: Unable to find size for global variable: init_user_ns (use will result in out of bounds access)
KLEE: WARNING: Type for RQF_MDS_STATFS is not sized
KLEE: WARNING: Unable to find size for global variable: RQF_MDS_STATFS (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_OBD_STATFS is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_OBD_STATFS (use will result in out of bounds access)
KLEE: WARNING: Type for RQF_MDS_GET_INFO is not sized
KLEE: WARNING: Unable to find size for global variable: RQF_MDS_GET_INFO (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_GETINFO_KEY is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_GETINFO_KEY (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_GETINFO_VALLEN is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_GETINFO_VALLEN (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_GETINFO_VAL is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_GETINFO_VAL (use will result in out of bounds access)
KLEE: WARNING: Type for RQF_MDS_HSM_CT_UNREGISTER is not sized
KLEE: WARNING: Unable to find size for global variable: RQF_MDS_HSM_CT_UNREGISTER (use will result in out of bounds access)
KLEE: WARNING: Type for RQF_MDS_HSM_PROGRESS is not sized
KLEE: WARNING: Unable to find size for global variable: RQF_MDS_HSM_PROGRESS (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_MDS_HSM_PROGRESS is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_MDS_HSM_PROGRESS (use will result in out of bounds access)
KLEE: WARNING: Type for RQF_MDS_HSM_STATE_GET is not sized
KLEE: WARNING: Unable to find size for global variable: RQF_MDS_HSM_STATE_GET (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_HSM_USER_STATE is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_HSM_USER_STATE (use will result in out of bounds access)
KLEE: WARNING: Type for RQF_MDS_HSM_STATE_SET is not sized
KLEE: WARNING: Unable to find size for global variable: RQF_MDS_HSM_STATE_SET (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_HSM_STATE_SET is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_HSM_STATE_SET (use will result in out of bounds access)
KLEE: WARNING: Type for RQF_MDS_HSM_ACTION is not sized
KLEE: WARNING: Unable to find size for global variable: RQF_MDS_HSM_ACTION (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_MDS_HSM_CURRENT_ACTION is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_MDS_HSM_CURRENT_ACTION (use will result in out of bounds access)
KLEE: WARNING: Type for RQF_MDS_HSM_REQUEST is not sized
KLEE: WARNING: Unable to find size for global variable: RQF_MDS_HSM_REQUEST (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_MDS_HSM_REQUEST is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_MDS_HSM_REQUEST (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_MDS_HSM_USER_ITEM is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_MDS_HSM_USER_ITEM (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_GENERIC_DATA is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_GENERIC_DATA (use will result in out of bounds access)
KLEE: WARNING: Type for RQF_MDS_SWAP_LAYOUTS is not sized
KLEE: WARNING: Unable to find size for global variable: RQF_MDS_SWAP_LAYOUTS (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_CAPA2 is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_CAPA2 (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_SWAP_LAYOUTS is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_SWAP_LAYOUTS (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_DLM_REP is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_DLM_REP (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_DLM_REQ is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_DLM_REQ (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_MDT_MD is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_MDT_MD (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_EADATA is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_EADATA (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_ACL is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_ACL (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_DLM_LVB is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_DLM_LVB (use will result in out of bounds access)
KLEE: WARNING: Type for RQF_LDLM_INTENT_GETATTR is not sized
KLEE: WARNING: Unable to find size for global variable: RQF_LDLM_INTENT_GETATTR (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_LDLM_INTENT is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_LDLM_INTENT (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_NAME is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_NAME (use will result in out of bounds access)
KLEE: WARNING: Type for RQF_MDS_GETATTR is not sized
KLEE: WARNING: Unable to find size for global variable: RQF_MDS_GETATTR (use will result in out of bounds access)
KLEE: ERROR: unable to load symbol(capa_cachep) while initializing globals.
KLEE: output directory is "/tmp/symbiotic-Ckc_cv/klee-out-0"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: function "mdc_enter_request" has inline asm
KLEE: WARNING ONCE: function "__client_obd_list_lock" has inline asm
KLEE: WARNING ONCE: function "__mdc_pack_body" has inline asm
KLEE: WARNING ONCE: function "llog_group_get_ctxt" has inline asm
KLEE: WARNING ONCE: function "mdc_close" has inline asm
KLEE: WARNING ONCE: function "mdc_done_writing" has inline asm
KLEE: WARNING ONCE: function "mdc_setattr" has inline asm
KLEE: WARNING ONCE: function "mdc_readpage" has inline asm
KLEE: WARNING ONCE: function "mdc_set_open_replay_data" has inline asm
KLEE: WARNING ONCE: function "mdc_clear_open_replay_data" has inline asm
KLEE: WARNING ONCE: function "mdc_unpack_capa" has inline asm
KLEE: WARNING ONCE: function "mdc_commit_open" has inline asm
KLEE: WARNING ONCE: function "posix_acl_release" has inline asm
KLEE: WARNING ONCE: function "capa_put" has inline asm
KLEE: WARNING ONCE: function "mdc_xattr_common" has inline asm
KLEE: WARNING ONCE: function "mdc_setattr_pack_rec" has inline asm
KLEE: WARNING ONCE: function "mdc_open_pack" has inline asm
KLEE: WARNING ONCE: function "__client_obd_list_lock___0" has inline asm
KLEE: WARNING: undefined reference to variable: RMF_ACL
KLEE: WARNING: undefined reference to variable: RMF_CAPA1
KLEE: WARNING: undefined reference to variable: RMF_CAPA2
KLEE: WARNING: undefined reference to variable: RMF_CLOSE_DATA
KLEE: WARNING: undefined reference to variable: RMF_DLM_LVB
KLEE: WARNING: undefined reference to variable: RMF_DLM_REP
KLEE: WARNING: undefined reference to variable: RMF_DLM_REQ
KLEE: WARNING: undefined reference to variable: RMF_EADATA
KLEE: WARNING: undefined reference to variable: RMF_GENERIC_DATA
KLEE: WARNING: undefined reference to variable: RMF_GETINFO_KEY
KLEE: WARNING: undefined reference to variable: RMF_GETINFO_VAL
KLEE: WARNING: undefined reference to variable: RMF_GETINFO_VALLEN
KLEE: WARNING: undefined reference to variable: RMF_HSM_STATE_SET
KLEE: WARNING: undefined reference to variable: RMF_HSM_USER_STATE
KLEE: WARNING: undefined reference to variable: RMF_LAYOUT_INTENT
KLEE: WARNING: undefined reference to variable: RMF_LDLM_INTENT
KLEE: WARNING: undefined reference to variable: RMF_LOGCOOKIES
KLEE: WARNING: undefined reference to variable: RMF_MDS_HSM_ARCHIVE
KLEE: WARNING: undefined reference to variable: RMF_MDS_HSM_CURRENT_ACTION
KLEE: WARNING: undefined reference to variable: RMF_MDS_HSM_PROGRESS
KLEE: WARNING: undefined reference to variable: RMF_MDS_HSM_REQUEST
KLEE: WARNING: undefined reference to variable: RMF_MDS_HSM_USER_ITEM
KLEE: WARNING: undefined reference to variable: RMF_MDT_BODY
KLEE: WARNING: undefined reference to variable: RMF_MDT_EPOCH
KLEE: WARNING: undefined reference to variable: RMF_MDT_MD
KLEE: WARNING: undefined reference to variable: RMF_NAME
KLEE: WARNING: undefined reference to variable: RMF_OBD_QUOTACTL
KLEE: WARNING: undefined reference to variable: RMF_OBD_STATFS
KLEE: WARNING: undefined reference to variable: RMF_REC_REINT
KLEE: WARNING: undefined reference to variable: RMF_SWAP_LAYOUTS
KLEE: WARNING: undefined reference to variable: RMF_SYMTGT
KLEE: WARNING: undefined reference to variable: RQF_LDLM_ENQUEUE
KLEE: WARNING: undefined reference to variable: RQF_LDLM_INTENT_GETATTR
KLEE: WARNING: undefined reference to variable: RQF_LDLM_INTENT_GETXATTR
KLEE: WARNING: undefined reference to variable: RQF_LDLM_INTENT_LAYOUT
KLEE: WARNING: undefined reference to variable: RQF_LDLM_INTENT_OPEN
KLEE: WARNING: undefined reference to variable: RQF_LDLM_INTENT_UNLINK
KLEE: WARNING: undefined reference to variable: RQF_MDS_CLOSE
KLEE: WARNING: undefined reference to variable: RQF_MDS_DONE_WRITING
KLEE: WARNING: undefined reference to variable: RQF_MDS_GETATTR
KLEE: WARNING: undefined reference to variable: RQF_MDS_GETATTR_NAME
KLEE: WARNING: undefined reference to variable: RQF_MDS_GETSTATUS
KLEE: WARNING: undefined reference to variable: RQF_MDS_GETXATTR
KLEE: WARNING: undefined reference to variable: RQF_MDS_GET_INFO
KLEE: WARNING: undefined reference to variable: RQF_MDS_HSM_ACTION
KLEE: WARNING: undefined reference to variable: RQF_MDS_HSM_CT_REGISTER
KLEE: WARNING: undefined reference to variable: RQF_MDS_HSM_CT_UNREGISTER
KLEE: WARNING: undefined reference to variable: RQF_MDS_HSM_PROGRESS
KLEE: WARNING: undefined reference to variable: RQF_MDS_HSM_REQUEST
KLEE: WARNING: undefined reference to variable: RQF_MDS_HSM_STATE_GET
KLEE: WARNING: undefined reference to variable: RQF_MDS_HSM_STATE_SET
KLEE: WARNING: undefined reference to variable: RQF_MDS_IS_SUBDIR
KLEE: WARNING: undefined reference to variable: RQF_MDS_QUOTACHECK
KLEE: WARNING: undefined reference to variable: RQF_MDS_QUOTACTL
KLEE: WARNING: undefined reference to variable: RQF_MDS_READPAGE
KLEE: WARNING: undefined reference to variable: RQF_MDS_REINT_CREATE_RMT_ACL
KLEE: WARNING: undefined reference to variable: RQF_MDS_REINT_LINK
KLEE: WARNING: undefined reference to variable: RQF_MDS_REINT_RENAME
KLEE: WARNING: undefined reference to variable: RQF_MDS_REINT_SETATTR
KLEE: WARNING: undefined reference to variable: RQF_MDS_REINT_SETXATTR
KLEE: WARNING: undefined reference to variable: RQF_MDS_REINT_UNLINK
KLEE: WARNING: undefined reference to variable: RQF_MDS_RELEASE_CLOSE
KLEE: WARNING: undefined reference to variable: RQF_MDS_STATFS
KLEE: WARNING: undefined reference to variable: RQF_MDS_SWAP_LAYOUTS
KLEE: WARNING: undefined reference to variable: RQF_MDS_SYNC
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: Type for RQF_MDS_QUOTACTL is not sized
KLEE: WARNING: Unable to find size for global variable: RQF_MDS_QUOTACTL (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_OBD_QUOTACTL is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_OBD_QUOTACTL (use will result in out of bounds access)
KLEE: WARNING: Type for RQF_MDS_QUOTACHECK is not sized
KLEE: WARNING: Unable to find size for global variable: RQF_MDS_QUOTACHECK (use will result in out of bounds access)
KLEE: WARNING: Type for RQF_MDS_HSM_CT_REGISTER is not sized
KLEE: WARNING: Unable to find size for global variable: RQF_MDS_HSM_CT_REGISTER (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_MDS_HSM_ARCHIVE is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_MDS_HSM_ARCHIVE (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_MDT_BODY is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_MDT_BODY (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_CAPA1 is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_CAPA1 (use will result in out of bounds access)
KLEE: WARNING: Type for init_user_ns is not sized
KLEE: WARNING: Unable to find size for global variable: init_user_ns (use will result in out of bounds access)
KLEE: WARNING: Type for RQF_MDS_STATFS is not sized
KLEE: WARNING: Unable to find size for global variable: RQF_MDS_STATFS (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_OBD_STATFS is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_OBD_STATFS (use will result in out of bounds access)
KLEE: WARNING: Type for RQF_MDS_GET_INFO is not sized
KLEE: WARNING: Unable to find size for global variable: RQF_MDS_GET_INFO (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_GETINFO_KEY is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_GETINFO_KEY (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_GETINFO_VALLEN is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_GETINFO_VALLEN (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_GETINFO_VAL is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_GETINFO_VAL (use will result in out of bounds access)
KLEE: WARNING: Type for RQF_MDS_HSM_CT_UNREGISTER is not sized
KLEE: WARNING: Unable to find size for global variable: RQF_MDS_HSM_CT_UNREGISTER (use will result in out of bounds access)
KLEE: WARNING: Type for RQF_MDS_HSM_PROGRESS is not sized
KLEE: WARNING: Unable to find size for global variable: RQF_MDS_HSM_PROGRESS (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_MDS_HSM_PROGRESS is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_MDS_HSM_PROGRESS (use will result in out of bounds access)
KLEE: WARNING: Type for RQF_MDS_HSM_STATE_GET is not sized
KLEE: WARNING: Unable to find size for global variable: RQF_MDS_HSM_STATE_GET (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_HSM_USER_STATE is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_HSM_USER_STATE (use will result in out of bounds access)
KLEE: WARNING: Type for RQF_MDS_HSM_STATE_SET is not sized
KLEE: WARNING: Unable to find size for global variable: RQF_MDS_HSM_STATE_SET (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_HSM_STATE_SET is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_HSM_STATE_SET (use will result in out of bounds access)
KLEE: WARNING: Type for RQF_MDS_HSM_ACTION is not sized
KLEE: WARNING: Unable to find size for global variable: RQF_MDS_HSM_ACTION (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_MDS_HSM_CURRENT_ACTION is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_MDS_HSM_CURRENT_ACTION (use will result in out of bounds access)
KLEE: WARNING: Type for RQF_MDS_HSM_REQUEST is not sized
KLEE: WARNING: Unable to find size for global variable: RQF_MDS_HSM_REQUEST (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_MDS_HSM_REQUEST is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_MDS_HSM_REQUEST (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_MDS_HSM_USER_ITEM is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_MDS_HSM_USER_ITEM (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_GENERIC_DATA is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_GENERIC_DATA (use will result in out of bounds access)
KLEE: WARNING: Type for RQF_MDS_SWAP_LAYOUTS is not sized
KLEE: WARNING: Unable to find size for global variable: RQF_MDS_SWAP_LAYOUTS (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_CAPA2 is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_CAPA2 (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_SWAP_LAYOUTS is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_SWAP_LAYOUTS (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_DLM_REP is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_DLM_REP (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_DLM_REQ is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_DLM_REQ (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_MDT_MD is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_MDT_MD (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_EADATA is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_EADATA (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_ACL is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_ACL (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_DLM_LVB is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_DLM_LVB (use will result in out of bounds access)
KLEE: WARNING: Type for RQF_LDLM_INTENT_GETATTR is not sized
KLEE: WARNING: Unable to find size for global variable: RQF_LDLM_INTENT_GETATTR (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_LDLM_INTENT is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_LDLM_INTENT (use will result in out of bounds access)
KLEE: WARNING: Type for RMF_NAME is not sized
KLEE: WARNING: Unable to find size for global variable: RMF_NAME (use will result in out of bounds access)
KLEE: WARNING: Type for RQF_MDS_GETATTR is not sized
KLEE: WARNING: Unable to find size for global variable: RQF_MDS_GETATTR (use will result in out of bounds access)
KLEE: ERROR: unable to load symbol(capa_cachep) while initializing globals.
Running the verifier failed
RESULT: unknown
INFO: Total time elapsed: 2.65834498405
