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--nfs--nfsv4.ko-ldv_main4_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.: 818 1392 11996 85015
Removed infinite loop in net_generic___3
Removed infinite loop in net_generic___4
Removed infinite loop in do_vfs_lock
Removed infinite loop in net_generic___1
Removed infinite loop in net_generic
Removed infinite loop in net_generic___2
Removed infinite loop in reserve_space
Removed infinite loop in net_generic___0
Removed infinite loop in encode_attrs
Removed infinite loop in encode_open
Removed infinite loop in encode_delegation_type
INFO: Compilation, preparation and instrumentation time: 2.79208517075
Removed calls to 'xdr_inline_pages' (function is undefined)
Removed calls to 'xdr_write_pages' (function is undefined)
Removed calls to 'xdr_terminate_string' (function is undefined)
Removed calls to 'xdr_set_scratch_buffer' (function is undefined)
Removed calls to 'xdr_enter_page' (function is undefined)
Removed calls to 'lockdep_rcu_suspicious' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function xdr_inline_decode as symbolic
Defining function printk as symbolic
Defining function nfs_lookup as symbolic
Defining function nfs_permission as symbolic
Defining function nfs_create as symbolic
Defining function nfs_link as symbolic
Defining function nfs_unlink as symbolic
Defining function nfs_symlink as symbolic
Defining function nfs_mkdir as symbolic
Defining function nfs_rmdir as symbolic
Defining function nfs_mknod as symbolic
Defining function nfs_rename as symbolic
Defining function nfs_setattr as symbolic
Defining function nfs_getattr as symbolic
Defining function generic_setxattr as symbolic
Defining function generic_getxattr as symbolic
Defining function generic_listxattr as symbolic
Defining function generic_removexattr as symbolic
Defining function nfs_atomic_open as symbolic
Removed calls to 'dput' (function is undefined)
Removed calls to 'free_pages' (function is undefined)
Removed calls to '__free_pages' (function is undefined)
Removed calls to 'rpc_shutdown_client' (function is undefined)
Removed calls to 'nfs_fattr_init' (function is undefined)
Removed calls to 'nfs_setattr_update_inode' (function is undefined)
Removed calls to 'nfs_access_set_mask' (function is undefined)
Removed calls to 'd_drop' (function is undefined)
Removed calls to 'd_instantiate' (function is undefined)
Removed calls to 'd_rehash' (function is undefined)
Removed calls to 'put_nfs_open_context' (function is undefined)
Removed calls to 'nfs_invalidate_atime' (function is undefined)
Removed calls to 'nfs_pageio_init_read' (function is undefined)
Removed calls to 'nfs_pageio_init' (function is undefined)
Removed calls to 'nfs_pageio_init_write' (function is undefined)
Removed calls to 'down_read' (function is undefined)
Removed calls to 'up_read' (function is undefined)
Removed calls to 'rpc_put_task' (function is undefined)
Removed calls to '__raw_spin_lock_init' (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)
Removed calls to 'rpc_init_wait_queue' (function is undefined)
Removed calls to 'nfs_free_client' (function is undefined)
Removed calls to 'nfs_mark_client_ready' (function is undefined)
Removed calls to 'nfs_put_client' (function is undefined)
Removed calls to 'rpc_destroy_wait_queue' (function is undefined)
Removed calls to 'nfs_init_timeout_values' (function is undefined)
Removed calls to 'nfs_free_server' (function is undefined)
Defining function nfs_clone_server as symbolic
Defining function nfs_alloc_server as symbolic
Removed calls to 'nfs_server_insert_lists' (function is undefined)
Defining function nfs_alloc_fattr as symbolic
Defining function nfs_probe_fsinfo as symbolic
Removed calls to 'module_put' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to 'rb_erase' (function is undefined)
Removed calls to 'ida_remove' (function is undefined)
Removed calls to 'put_rpccred' (function is undefined)
Removed calls to 'synchronize_sched' (function is undefined)
Removed calls to 'lock_acquire' (function is undefined)
Defining function debug_lockdep_rcu_enabled as symbolic
Removed calls to 'lock_release' (function is undefined)
Defining function rcu_is_cpu_idle as symbolic
Defining function rcu_lockdep_current_cpu_online as symbolic
Defining function lock_is_held as symbolic
Removed calls to 'iput' (function is undefined)
Removed calls to '__module_get' (function is undefined)
Removed calls to 'wake_up_bit' (function is undefined)
Removed calls to 'rpc_wake_up' (function is undefined)
Defining function rpc_peeraddr2str as symbolic
Defining function snprintf as symbolic
Removed calls to 'msleep' (function is undefined)
Removed calls to '__module_put_and_exit' (function is undefined)
Defining function kthread_create_on_node as symbolic
Defining function wake_up_process as symbolic
Defining function allow_signal as symbolic
Removed calls to 'down_write' (function is undefined)
Removed calls to 'lock_flocks' (function is undefined)
Removed calls to 'unlock_flocks' (function is undefined)
Removed calls to 'up_write' (function is undefined)
Defining function ___ratelimit as symbolic
Removed calls to 'complete' (function is undefined)
Defining function find_last_bit as symbolic
Defining function rpc_wake_up_first as symbolic
Defining function find_first_zero_bit as symbolic
Removed calls to 'kfree_call_rcu' (function is undefined)
Defining function igrab as symbolic
Defining function rb_first as symbolic
Defining function rb_next as symbolic
Defining function _atomic_dec_and_lock as symbolic
Defining function rpc_call_sync as symbolic
Defining function wait_for_completion_interruptible as symbolic
Defining function rpc_run_task as symbolic
Defining function mod_delayed_work as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Defining function nfs_wait_bit_killable as symbolic
Defining function out_of_line_wait_on_bit as symbolic
Defining function schedule_timeout_killable as symbolic
Defining function __refrigerator as symbolic
Defining function freezing_slow_path as symbolic
Defining function nfs_post_op_update_inode_force_wcc as symbolic
Defining function nfs_refresh_inode as symbolic
Defining function __rpc_wait_for_completion_task as symbolic
Defining function get_nfs_open_context as symbolic
Removed calls to 'rpc_wake_up_queued_task' (function is undefined)
Removed calls to 'ida_simple_remove' (function is undefined)
Defining function ida_simple_get as symbolic
Defining function ktime_get as symbolic
Removed calls to 'nfs_sb_deactive' (function is undefined)
Removed calls to 'nfs_sb_active' (function is undefined)
Defining function nfs_fhget as symbolic
Removed calls to 'ihold' (function is undefined)
Removed calls to '__list_add_rcu' (function is undefined)
Defining function nfs_may_open as symbolic
Defining function kstrtoll as symbolic
Removed calls to 'revert_creds' (function is undefined)
Removed calls to 'key_put' (function is undefined)
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function override_creds as symbolic
Defining function request_key_with_auxdata as symbolic
Defining function request_key as symbolic
Defining function key_validate as symbolic
Defining function kstrtoull as symbolic
Defining function dget_parent as symbolic
Defining function nfs_init_server_rpcclient as symbolic
Defining function nfs_get_client as symbolic
Removed calls to 'rpc_put_sb_net' (function is undefined)
Removed calls to 'rpc_destroy_pipe_data' (function is undefined)
Defining function rpc_get_sb_net as symbolic
Defining function rpc_unlink as symbolic
Removed calls to 'svc_exit_thread' (function is undefined)
Removed calls to 'svc_shutdown_net' (function is undefined)
Defining function kthread_stop as symbolic
Removed calls to 'xprt_destroy_backchannel' (function is undefined)
Defining function cancel_delayed_work_sync as symbolic
Defining function nfs_create_rpc_client as symbolic
Defining function rpc_localaddr as symbolic
Defining function rpc_ntop as symbolic
Defining function strlcpy as symbolic
Removed calls to '__mutex_init' (function is undefined)
Defining function rpcauth_list_flavors as symbolic
Defining function rpc_clone_client_set_auth as symbolic
Removed calls to 'rpc_init_priority_wait_queue' (function is undefined)
Defining function xprt_setup_backchannel as symbolic
Removed calls to 'svc_rpcb_cleanup' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'svc_xprt_put' (function is undefined)
Removed calls to 'svc_sock_update_bufs' (function is undefined)
Removed calls to 'svc_destroy' (function is undefined)
Defining function sprintf as symbolic
Removed calls to '_raw_spin_unlock_bh' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to 'prepare_to_wait' (function is undefined)
Removed calls to '_raw_spin_lock_bh' (function is undefined)
Defining function autoremove_wake_function as symbolic
Defining function set_freezable as symbolic
Defining function bc_svc_process as symbolic
Defining function kthread_should_stop as symbolic
Defining function svc_prepare_thread as symbolic
Defining function svc_recv as symbolic
Defining function svc_process as symbolic
Defining function svc_bind as symbolic
Defining function svc_create_xprt as symbolic
Defining function svc_create as symbolic
Defining function rpc_mkpipe_data as symbolic
Defining function rpc_mkpipe_dentry as symbolic
Defining function nfs_alloc_client as symbolic
Defining function idr_pre_get as symbolic
Defining function idr_get_new as symbolic
Defining function nfs_wb_all as symbolic
Removed calls to 'nfs_access_add_cache' (function is undefined)
Removed calls to 'rb_insert_color' (function is undefined)
Defining function nfs_post_op_update_inode as symbolic
Defining function rpc_call_async as symbolic
Removed calls to 'nfs_force_lookup_revalidate' (function is undefined)
Removed calls to '__fscache_invalidate' (function is undefined)
Defining function ida_pre_get as symbolic
Defining function ida_get_new as symbolic
Defining function posix_lock_file_wait as symbolic
Defining function flock_lock_file_wait as symbolic
Removed calls to 'rpc_delay' (function is undefined)
Defining function rpc_restart_call_prepare as symbolic
Defining function rpc_restart_call as symbolic
Removed calls to 'rpc_call_start' (function is undefined)
Removed calls to 'rpc_sleep_on_priority' (function is undefined)
Removed calls to 'rpc_sleep_on' (function is undefined)
Defining function xdr_stream_pos as symbolic
Defining function kmemdup as symbolic
Defining function __request_module as symbolic
Defining function try_module_get as symbolic
Defining function current_umask as symbolic
Defining function nfs_instantiate as symbolic
Defining function alloc_nfs_open_context as symbolic
Removed calls to 'put_page' (function is undefined)
Removed calls to 'gss_mech_put' (function is undefined)
Defining function gss_mech_get_by_OID as symbolic
Defining function gss_svc_to_pseudoflavor as symbolic
Defining function alloc_pages_current as symbolic
Removed calls to 'mntput' (function is undefined)
Defining function mount_subtree as symbolic
Defining function vfs_kern_mount as symbolic
Defining function nfs_do_submount as symbolic
Defining function __get_free_pages as symbolic
Defining function rpc_net_ns as symbolic
Defining function rpc_pton as symbolic
Defining function nfs_dns_resolve_name as symbolic
Defining function nfs_path as symbolic
Defining function rpc_clone_client as symbolic
Defining function nfs_file_llseek as symbolic
Defining function do_sync_read as symbolic
Defining function do_sync_write as symbolic
Defining function nfs_file_read as symbolic
Defining function nfs_file_write as symbolic
Defining function nfs_file_mmap as symbolic
Removed calls to 'nfs_file_set_open_context' (function is undefined)
Removed calls to 'nfs_fscache_set_inode_cookie' (function is undefined)
Defining function nfs_file_flush as symbolic
Defining function nfs_file_release as symbolic
Defining function nfs_lock as symbolic
Defining function nfs_check_flags as symbolic
Defining function nfs_flock as symbolic
Defining function nfs_file_splice_write as symbolic
Defining function nfs_file_splice_read as symbolic
Defining function nfs_setlease as symbolic
Defining function filemap_write_and_wait_range as symbolic
Defining function nfs_file_fsync_commit as symbolic
Removed calls to '__mark_inode_dirty' (function is undefined)
Defining function out_of_line_wait_on_bit_lock as symbolic
Removed calls to 'nfs_sb_deactive_async' (function is undefined)
Removed calls to 'rpc_put_task_async' (function is undefined)
Removed calls to 'rpc_exit' (function is undefined)
Defining function rpcauth_create as symbolic
Defining function idr_replace as symbolic
Defining function scnprintf as symbolic
Defining function nfs_wait_client_init_complete as symbolic
Removed calls to 'nfs_zap_acl_cache' (function is undefined)
Removed calls to '_copy_from_pages' (function is undefined)
Removed calls to 'nfs_access_zap_cache' (function is undefined)
Defining function nfs_revalidate_inode as symbolic
Defining function nfs_alloc_inode as symbolic
Defining function nfs_drop_inode as symbolic
Removed calls to 'truncate_inode_pages' (function is undefined)
Removed calls to 'clear_inode' (function is undefined)
Removed calls to 'nfs_clear_inode' (function is undefined)
Defining function nfs_statfs as symbolic
Defining function nfs_remount as symbolic
Defining function nfs_show_options as symbolic
Defining function nfs_show_devname as symbolic
Defining function nfs_show_path as symbolic
Defining function nfs_show_stats as symbolic
Defining function nfs_write_inode as symbolic
Defining function nfs_set_sb_security as symbolic
Defining function nfs_fs_mount_common as symbolic
Defining function nfs_clone_sb_security as symbolic
Defining function nfs_alloc_fhandle as symbolic
Removed calls to 'nfs_server_copy_userdata' (function is undefined)
Defining function rpc_protocol as symbolic
Defining function rpc_pipe_generic_upcall as symbolic
Removed calls to 'might_fault' (function is undefined)
Removed calls to 'key_set_timeout' (function is undefined)
Removed calls to 'complete_request_key' (function is undefined)
Defining function strnlen as symbolic
Defining function key_instantiate_and_link as symbolic
Defining function _copy_from_user as symbolic
Defining function user_instantiate as symbolic
Defining function user_match as symbolic
Defining function user_read as symbolic
Defining function rpc_queue_upcall as symbolic
Defining function match_token as symbolic
Defining function match_strlcpy as symbolic
Defining function match_int as symbolic
Defining function rpc_rmdir as symbolic
Removed calls to 'xdr_init_decode' (function is undefined)
Removed calls to 'xdr_init_encode' (function is undefined)
Defining function xdr_reserve_space as symbolic
Defining function xdr_encode_opaque as symbolic
Defining function idr_find as symbolic
Defining function nfs_sockaddr_match_ipaddr as symbolic
Defining function filemap_flush as symbolic
Defining function proc_dointvec_minmax as symbolic
Defining function proc_dointvec_jiffies as symbolic
Defining function xdr_encode_opaque_fixed as symbolic
Defining function xdr_read_pages as symbolic
Removed calls to 'ldv_handler_precall' (function is undefined)
Defining function mutex_trylock as symbolic
Removed calls to 'rpc_pipefs_notifier_unregister' (function is undefined)
Removed calls to 'register_nfs_version' (function is undefined)
Removed calls to 'unregister_nfs_version' (function is undefined)
Removed calls to 'unregister_sysctl_table' (function is undefined)
Removed calls to 'key_revoke' (function is undefined)
Removed calls to 'unregister_key_type' (function is undefined)
Removed calls to '__invalid_creds' (function is undefined)
Removed calls to '__put_cred' (function is undefined)
Defining function creds_are_invalid as symbolic
Defining function register_sysctl_table as symbolic
Defining function rpc_pipefs_notifier_register as symbolic
Defining function prepare_kernel_cred as symbolic
Defining function keyring_alloc as symbolic
Defining function register_key_type as symbolic
Removed calls to 'ldv_check_return_value' (function is undefined)
Removed calls to 'nfs_pageio_reset_read_mds' (function is undefined)
Defining function nfs_dreq_bytes_left as symbolic
Removed calls to 'nfs_pageio_reset_write_mds' (function is undefined)
Defining function nfs_generic_pg_test as symbolic
Removed calls to 'nfs_pageio_complete' (function is undefined)
Defining function nfs_pageio_add_request as symbolic
Removed calls to 'nfs_pgheader_init' (function is undefined)
Removed calls to 'nfs_writedata_release' (function is undefined)
Defining function nfs_writehdr_alloc as symbolic
Removed calls to 'nfs_writehdr_free' (function is undefined)
Defining function nfs_generic_flush as symbolic
Removed calls to 'nfs_readdata_release' (function is undefined)
Defining function nfs_readhdr_alloc as symbolic
Removed calls to 'nfs_readhdr_free' (function is undefined)
Defining function nfs_generic_pagein as symbolic
Linked our definitions to these undefined functions:
  memchr
  memcmp
  strchr
  strcmp
  strcpy
  strlen
  strncmp
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 3.02095198631
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 1324 977 6967 55323
INFO: Starting verification
KLEE: WARNING ONCE: function "nfs4_xdr_enc_exchange_id" has inline asm
KLEE: WARNING ONCE: function "nfs4_xdr_enc_create_session" has inline asm
KLEE: WARNING ONCE: function "nfs4_proc_readdir" has inline asm
KLEE: WARNING ONCE: function "nfs4_proc_lock" has inline asm
KLEE: WARNING ONCE: function "nfs4_have_delegation" has inline asm
KLEE: WARNING ONCE: function "nfs4_init_client" has inline asm
KLEE: WARNING ONCE: function "nfs4_free_client" has inline asm
KLEE: WARNING ONCE: function "nfs4_set_client" has inline asm
KLEE: WARNING ONCE: function "nfs4_init_session" has inline asm
KLEE: WARNING ONCE: function "nfs_server_return_all_delegations" has inline asm
KLEE: WARNING ONCE: function "unset_pnfs_layoutdriver" has inline asm
KLEE: WARNING ONCE: function "nfs4_deviceid_purge_client" has inline asm
KLEE: WARNING ONCE: function "rcu_read_lock___9" has inline asm
KLEE: WARNING ONCE: function "rcu_read_unlock___9" 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 "nfs_client_return_marked_delegations" has inline asm
KLEE: WARNING ONCE: function "nfs4_schedule_state_manager" has inline asm
KLEE: WARNING ONCE: function "rcu_read_lock___1" has inline asm
KLEE: WARNING ONCE: function "rcu_read_unlock___1" has inline asm
KLEE: WARNING ONCE: function "nfs4_run_state_manager" has inline asm
KLEE: WARNING ONCE: function "nfs4_handle_reclaim_lease_error" has inline asm
KLEE: WARNING ONCE: function "nfs4_begin_drain_session" has inline asm
KLEE: WARNING ONCE: function "nfs4_get_exchange_id_cred" has inline asm
KLEE: WARNING ONCE: function "nfs4_recovery_handle_error" has inline asm
KLEE: WARNING ONCE: function "nfs41_finish_session_reset" has inline asm
KLEE: WARNING ONCE: function "nfs4_get_setclientid_cred" has inline asm
KLEE: WARNING ONCE: function "nfs4_do_reclaim" has inline asm
KLEE: WARNING ONCE: function "nfs4_end_drain_session" has inline asm
KLEE: WARNING ONCE: function "nfs4_alloc_slot" has inline asm
KLEE: WARNING ONCE: function "nfs4_free_slot" has inline asm
KLEE: WARNING ONCE: function "nfs4_state_clear_reclaim_reboot" has inline asm
KLEE: WARNING ONCE: function "nfs4_schedule_state_renewal" has inline asm
KLEE: WARNING ONCE: function "nfs40_handle_cb_pathdown" has inline asm
KLEE: WARNING ONCE: function "nfs_delegation_mark_reclaim" has inline asm
KLEE: WARNING ONCE: function "nfs4_state_mark_reclaim_reboot" has inline asm
KLEE: WARNING ONCE: function "nfs4_state_mark_reclaim_helper" has inline asm
KLEE: WARNING ONCE: function "nfs_expire_all_delegation_types" has inline asm
KLEE: WARNING ONCE: function "nfs4_state_mark_reclaim_nograce" has inline asm
KLEE: WARNING ONCE: function "pnfs_destroy_all_layouts" has inline asm
KLEE: WARNING ONCE: function "nfs4_deviceid_mark_client_invalid" has inline asm
KLEE: WARNING ONCE: function "pnfs_destroy_layout" has inline asm
KLEE: WARNING ONCE: function "mark_lseg_invalid" has inline asm
KLEE: WARNING ONCE: function "pnfs_layout_remove_lseg" has inline asm
KLEE: WARNING ONCE: function "nfs4_handle_exception" has inline asm
KLEE: WARNING ONCE: function "nfs4_schedule_stateid_recovery" has inline asm
KLEE: WARNING ONCE: function "nfs4_schedule_lease_recovery" has inline asm
KLEE: WARNING ONCE: function "nfs4_schedule_session_recovery" has inline asm
KLEE: WARNING ONCE: function "freezer_count" has inline asm
KLEE: WARNING ONCE: function "nfs4_wait_clnt_recover" has inline asm
KLEE: WARNING ONCE: function "nfs_inode_find_state_and_recover" has inline asm
KLEE: WARNING ONCE: function "_nfs4_do_setlk" has inline asm
KLEE: WARNING ONCE: function "nfs4_get_lock_state" has inline asm
KLEE: WARNING ONCE: function "nfs4_open_recoverdata_alloc" has inline asm
KLEE: WARNING ONCE: function "nfs4_open_recover" has inline asm
KLEE: WARNING ONCE: function "nfs4_opendata_put" has inline asm
KLEE: WARNING ONCE: function "nfs4_run_open_task" has inline asm
KLEE: WARNING ONCE: function "_nfs4_proc_open_confirm" has inline asm
KLEE: WARNING ONCE: function "nfs4_opendata_to_nfs4_state" has inline asm
KLEE: WARNING ONCE: function "__nfs4_close" has inline asm
KLEE: WARNING ONCE: function "pnfs_roc" has inline asm
KLEE: WARNING ONCE: function "nfs4_get_open_state" has inline asm
KLEE: WARNING ONCE: function "update_open_stateid" has inline asm
KLEE: WARNING ONCE: function "__update_open_stateid" has inline asm
KLEE: WARNING ONCE: function "nfs_set_open_stateid_locked" has inline asm
KLEE: WARNING ONCE: function "nfs_inode_set_delegation" has inline asm
KLEE: WARNING ONCE: function "nfs_inode_reclaim_delegation" has inline asm
KLEE: WARNING ONCE: function "rcu_read_lock___3" has inline asm
KLEE: WARNING ONCE: function "rcu_read_unlock___3" has inline asm
KLEE: WARNING ONCE: function "nfs4_opendata_alloc" has inline asm
KLEE: WARNING ONCE: function "net_generic___3" has inline asm
KLEE: WARNING ONCE: function "nfs41_callback_svc" has inline asm
KLEE: WARNING ONCE: function "net_generic___4" has inline asm
KLEE: WARNING ONCE: function "nfs4_renew_state" has inline asm
KLEE: WARNING ONCE: function "nfs_expire_unreferenced_delegations" has inline asm
KLEE: WARNING ONCE: function "nfs4_do_open" has inline asm
KLEE: WARNING ONCE: function "nfs4_get_state_owner" has inline asm
KLEE: WARNING ONCE: function "nfs4_do_setattr" has inline asm
KLEE: WARNING ONCE: function "nfs4_select_rw_stateid" has inline asm
KLEE: WARNING ONCE: function "nfs4_copy_delegation_stateid" has inline asm
KLEE: WARNING ONCE: function "nfs4_put_lock_state" has inline asm
KLEE: WARNING ONCE: function "do_vfs_lock" has inline asm
KLEE: WARNING ONCE: function "nfs4_do_unlck" has inline asm
KLEE: WARNING ONCE: function "nfs41_sequence_done" has inline asm
KLEE: WARNING ONCE: function "nfs4_async_handle_error" has inline asm
KLEE: WARNING ONCE: function "set_pnfs_layoutdriver" has inline asm
KLEE: WARNING ONCE: function "_pnfs_return_layout" has inline asm
KLEE: WARNING ONCE: function "nfs_follow_remote_path" has inline asm
KLEE: WARNING ONCE: function "pnfs_layoutcommit_inode" has inline asm
KLEE: WARNING ONCE: function "nfs4_open_prepare" has inline asm
KLEE: WARNING ONCE: function "nfs4_close_done" has inline asm
KLEE: WARNING ONCE: function "pnfs_roc_release" has inline asm
KLEE: WARNING ONCE: function "nfs4_lock_done" has inline asm
KLEE: WARNING ONCE: function "pnfs_choose_layoutget_stateid" has inline asm
KLEE: WARNING ONCE: function "nfs4_layoutcommit_release" has inline asm
KLEE: WARNING ONCE: function "pnfs_put_lseg" has inline asm
KLEE: WARNING ONCE: function "nfs4_init_clientid" has inline asm
KLEE: WARNING ONCE: function "nfs40_discover_server_trunking" has inline asm
KLEE: WARNING ONCE: function "net_generic___1" has inline asm
KLEE: WARNING ONCE: function "nfs40_walk_client_list" has inline asm
KLEE: WARNING ONCE: function "nfs4_init_boot_verifier" has inline asm
KLEE: WARNING ONCE: function "nfs4_proc_async_renew" has inline asm
KLEE: WARNING ONCE: function "nfs4_get_renew_cred_locked" has inline asm
KLEE: WARNING ONCE: function "nfs41_init_clientid" has inline asm
KLEE: WARNING ONCE: function "nfs41_discover_server_trunking" has inline asm
KLEE: WARNING ONCE: function "nfs4_proc_exchange_id" has inline asm
KLEE: WARNING ONCE: function "nfs41_walk_client_list" has inline asm
KLEE: WARNING ONCE: function "nfs41_open_expired" has inline asm
KLEE: WARNING ONCE: function "nfs41_lock_expired" has inline asm
KLEE: WARNING ONCE: function "nfs4_get_machine_cred_locked" has inline asm
KLEE: WARNING ONCE: function "_nfs41_proc_sequence" has inline asm
KLEE: WARNING ONCE: function "nfs41_handle_sequence_flag_errors" has inline asm
KLEE: WARNING ONCE: function "nfs4_fl_copy_lock" has inline asm
KLEE: WARNING ONCE: function "rpc_pipefs_event" has inline asm
KLEE: WARNING ONCE: function "nfs4_find_client_ident" has inline asm
KLEE: WARNING ONCE: function "nfs4_callback_recallslot" has inline asm
KLEE: WARNING ONCE: function "nfs4_callback_sequence" has inline asm
KLEE: WARNING ONCE: function "rcu_read_lock___5" has inline asm
KLEE: WARNING ONCE: function "rcu_read_unlock___5" has inline asm
KLEE: WARNING ONCE: function "nfs4_delete_deviceid" has inline asm
KLEE: WARNING ONCE: function "nfs4_find_client_sessionid" has inline asm
KLEE: WARNING ONCE: function "do_callback_layoutrecall" has inline asm
KLEE: WARNING ONCE: function "nfs_async_inode_return_delegation" has inline asm
KLEE: WARNING ONCE: function "reserve_space" has inline asm
KLEE: WARNING ONCE: function "encode_attrs" has inline asm
KLEE: WARNING ONCE: function "encode_open" has inline asm
KLEE: WARNING ONCE: function "pnfs_get_layout_hdr" has inline asm
KLEE: WARNING ONCE: function "nfs_mark_delegation_referenced" has inline asm
KLEE: WARNING ONCE: function "nfs41_server_notify_highest_slotid_update" has inline asm
KLEE: WARNING ONCE: function "nfs41_server_notify_target_slotid_update" has inline asm
KLEE: WARNING ONCE: function "pnfs_layout_process" has inline asm
KLEE: WARNING ONCE: function "ldv_main2_sequence_infinite_withcheck_stateful" has inline asm
KLEE: WARNING ONCE: function "nfs_idmap_init" has inline asm
KLEE: WARNING ONCE: function "put_cred" has inline asm
KLEE: WARNING ONCE: function "nfs4_init_ds_session" has inline asm
KLEE: WARNING ONCE: function "pnfs_update_layout" has inline asm
KLEE: WARNING ONCE: function "pnfs_layout_io_set_failed" has inline asm
KLEE: WARNING ONCE: function "pnfs_ld_write_done" has inline asm
KLEE: WARNING ONCE: function "pnfs_set_layoutcommit" has inline asm
KLEE: WARNING ONCE: function "pnfs_generic_pg_writepages" has inline asm
KLEE: WARNING ONCE: function "pnfs_ld_read_done" has inline asm
KLEE: WARNING ONCE: function "pnfs_generic_pg_readpages" has inline asm
KLEE: WARNING ONCE: function "_find_get_deviceid" has inline asm
KLEE: WARNING ONCE: function "nfs4_insert_deviceid_node" has inline asm
KLEE: WARNING ONCE: function "nfs4_put_deviceid_node" has inline asm
KLEE: WARNING ONCE: function "nfs4_mark_deviceid_unavailable" has inline asm
KLEE: WARNING ONCE: function "nfs4_test_deviceid_unavailable" has inline asm
KLEE: WARNING: undefined reference to function: delayed_work_timer_fn
KLEE: WARNING: undefined reference to function: nfs_destroy_inode
KLEE: WARNING: undefined reference to function: nfs_fill_super
KLEE: WARNING: undefined reference to function: nfs_kill_super
KLEE: WARNING: undefined reference to function: nfs_put_super
KLEE: WARNING: undefined reference to function: nfs_umount_begin
KLEE: WARNING: undefined reference to variable: nfsiod_workqueue
KLEE: WARNING: undefined reference to variable: system_wq
KLEE: WARNING: undefined reference to function: user_describe
KLEE: WARNING: undefined reference to function: user_destroy
KLEE: WARNING: undefined reference to function: user_revoke
KLEE: ERROR: unable to load symbol(system_wq) while initializing globals.
KLEE: output directory is "/tmp/symbiotic-IRww_a/klee-out-0"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: function "nfs4_xdr_enc_exchange_id" has inline asm
KLEE: WARNING ONCE: function "nfs4_xdr_enc_create_session" has inline asm
KLEE: WARNING ONCE: function "nfs4_proc_readdir" has inline asm
KLEE: WARNING ONCE: function "nfs4_proc_lock" has inline asm
KLEE: WARNING ONCE: function "nfs4_have_delegation" has inline asm
KLEE: WARNING ONCE: function "nfs4_init_client" has inline asm
KLEE: WARNING ONCE: function "nfs4_free_client" has inline asm
KLEE: WARNING ONCE: function "nfs4_set_client" has inline asm
KLEE: WARNING ONCE: function "nfs4_init_session" has inline asm
KLEE: WARNING ONCE: function "nfs_server_return_all_delegations" has inline asm
KLEE: WARNING ONCE: function "unset_pnfs_layoutdriver" has inline asm
KLEE: WARNING ONCE: function "nfs4_deviceid_purge_client" has inline asm
KLEE: WARNING ONCE: function "rcu_read_lock___9" has inline asm
KLEE: WARNING ONCE: function "rcu_read_unlock___9" 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 "nfs_client_return_marked_delegations" has inline asm
KLEE: WARNING ONCE: function "nfs4_schedule_state_manager" has inline asm
KLEE: WARNING ONCE: function "rcu_read_lock___1" has inline asm
KLEE: WARNING ONCE: function "rcu_read_unlock___1" has inline asm
KLEE: WARNING ONCE: function "nfs4_run_state_manager" has inline asm
KLEE: WARNING ONCE: function "nfs4_handle_reclaim_lease_error" has inline asm
KLEE: WARNING ONCE: function "nfs4_begin_drain_session" has inline asm
KLEE: WARNING ONCE: function "nfs4_get_exchange_id_cred" has inline asm
KLEE: WARNING ONCE: function "nfs4_recovery_handle_error" has inline asm
KLEE: WARNING ONCE: function "nfs41_finish_session_reset" has inline asm
KLEE: WARNING ONCE: function "nfs4_get_setclientid_cred" has inline asm
KLEE: WARNING ONCE: function "nfs4_do_reclaim" has inline asm
KLEE: WARNING ONCE: function "nfs4_end_drain_session" has inline asm
KLEE: WARNING ONCE: function "nfs4_alloc_slot" has inline asm
KLEE: WARNING ONCE: function "nfs4_free_slot" has inline asm
KLEE: WARNING ONCE: function "nfs4_state_clear_reclaim_reboot" has inline asm
KLEE: WARNING ONCE: function "nfs4_schedule_state_renewal" has inline asm
KLEE: WARNING ONCE: function "nfs40_handle_cb_pathdown" has inline asm
KLEE: WARNING ONCE: function "nfs_delegation_mark_reclaim" has inline asm
KLEE: WARNING ONCE: function "nfs4_state_mark_reclaim_reboot" has inline asm
KLEE: WARNING ONCE: function "nfs4_state_mark_reclaim_helper" has inline asm
KLEE: WARNING ONCE: function "nfs_expire_all_delegation_types" has inline asm
KLEE: WARNING ONCE: function "nfs4_state_mark_reclaim_nograce" has inline asm
KLEE: WARNING ONCE: function "pnfs_destroy_all_layouts" has inline asm
KLEE: WARNING ONCE: function "nfs4_deviceid_mark_client_invalid" has inline asm
KLEE: WARNING ONCE: function "pnfs_destroy_layout" has inline asm
KLEE: WARNING ONCE: function "mark_lseg_invalid" has inline asm
KLEE: WARNING ONCE: function "pnfs_layout_remove_lseg" has inline asm
KLEE: WARNING ONCE: function "nfs4_handle_exception" has inline asm
KLEE: WARNING ONCE: function "nfs4_schedule_stateid_recovery" has inline asm
KLEE: WARNING ONCE: function "nfs4_schedule_lease_recovery" has inline asm
KLEE: WARNING ONCE: function "nfs4_schedule_session_recovery" has inline asm
KLEE: WARNING ONCE: function "freezer_count" has inline asm
KLEE: WARNING ONCE: function "nfs4_wait_clnt_recover" has inline asm
KLEE: WARNING ONCE: function "nfs_inode_find_state_and_recover" has inline asm
KLEE: WARNING ONCE: function "_nfs4_do_setlk" has inline asm
KLEE: WARNING ONCE: function "nfs4_get_lock_state" has inline asm
KLEE: WARNING ONCE: function "nfs4_open_recoverdata_alloc" has inline asm
KLEE: WARNING ONCE: function "nfs4_open_recover" has inline asm
KLEE: WARNING ONCE: function "nfs4_opendata_put" has inline asm
KLEE: WARNING ONCE: function "nfs4_run_open_task" has inline asm
KLEE: WARNING ONCE: function "_nfs4_proc_open_confirm" has inline asm
KLEE: WARNING ONCE: function "nfs4_opendata_to_nfs4_state" has inline asm
KLEE: WARNING ONCE: function "__nfs4_close" has inline asm
KLEE: WARNING ONCE: function "pnfs_roc" has inline asm
KLEE: WARNING ONCE: function "nfs4_get_open_state" has inline asm
KLEE: WARNING ONCE: function "update_open_stateid" has inline asm
KLEE: WARNING ONCE: function "__update_open_stateid" has inline asm
KLEE: WARNING ONCE: function "nfs_set_open_stateid_locked" has inline asm
KLEE: WARNING ONCE: function "nfs_inode_set_delegation" has inline asm
KLEE: WARNING ONCE: function "nfs_inode_reclaim_delegation" has inline asm
KLEE: WARNING ONCE: function "rcu_read_lock___3" has inline asm
KLEE: WARNING ONCE: function "rcu_read_unlock___3" has inline asm
KLEE: WARNING ONCE: function "nfs4_opendata_alloc" has inline asm
KLEE: WARNING ONCE: function "net_generic___3" has inline asm
KLEE: WARNING ONCE: function "nfs41_callback_svc" has inline asm
KLEE: WARNING ONCE: function "net_generic___4" has inline asm
KLEE: WARNING ONCE: function "nfs4_renew_state" has inline asm
KLEE: WARNING ONCE: function "nfs_expire_unreferenced_delegations" has inline asm
KLEE: WARNING ONCE: function "nfs4_do_open" has inline asm
KLEE: WARNING ONCE: function "nfs4_get_state_owner" has inline asm
KLEE: WARNING ONCE: function "nfs4_do_setattr" has inline asm
KLEE: WARNING ONCE: function "nfs4_select_rw_stateid" has inline asm
KLEE: WARNING ONCE: function "nfs4_copy_delegation_stateid" has inline asm
KLEE: WARNING ONCE: function "nfs4_put_lock_state" has inline asm
KLEE: WARNING ONCE: function "do_vfs_lock" has inline asm
KLEE: WARNING ONCE: function "nfs4_do_unlck" has inline asm
KLEE: WARNING ONCE: function "nfs41_sequence_done" has inline asm
KLEE: WARNING ONCE: function "nfs4_async_handle_error" has inline asm
KLEE: WARNING ONCE: function "set_pnfs_layoutdriver" has inline asm
KLEE: WARNING ONCE: function "_pnfs_return_layout" has inline asm
KLEE: WARNING ONCE: function "nfs_follow_remote_path" has inline asm
KLEE: WARNING ONCE: function "pnfs_layoutcommit_inode" has inline asm
KLEE: WARNING ONCE: function "nfs4_open_prepare" has inline asm
KLEE: WARNING ONCE: function "nfs4_close_done" has inline asm
KLEE: WARNING ONCE: function "pnfs_roc_release" has inline asm
KLEE: WARNING ONCE: function "nfs4_lock_done" has inline asm
KLEE: WARNING ONCE: function "pnfs_choose_layoutget_stateid" has inline asm
KLEE: WARNING ONCE: function "nfs4_layoutcommit_release" has inline asm
KLEE: WARNING ONCE: function "pnfs_put_lseg" has inline asm
KLEE: WARNING ONCE: function "nfs4_init_clientid" has inline asm
KLEE: WARNING ONCE: function "nfs40_discover_server_trunking" has inline asm
KLEE: WARNING ONCE: function "net_generic___1" has inline asm
KLEE: WARNING ONCE: function "nfs40_walk_client_list" has inline asm
KLEE: WARNING ONCE: function "nfs4_init_boot_verifier" has inline asm
KLEE: WARNING ONCE: function "nfs4_proc_async_renew" has inline asm
KLEE: WARNING ONCE: function "nfs4_get_renew_cred_locked" has inline asm
KLEE: WARNING ONCE: function "nfs41_init_clientid" has inline asm
KLEE: WARNING ONCE: function "nfs41_discover_server_trunking" has inline asm
KLEE: WARNING ONCE: function "nfs4_proc_exchange_id" has inline asm
KLEE: WARNING ONCE: function "nfs41_walk_client_list" has inline asm
KLEE: WARNING ONCE: function "nfs41_open_expired" has inline asm
KLEE: WARNING ONCE: function "nfs41_lock_expired" has inline asm
KLEE: WARNING ONCE: function "nfs4_get_machine_cred_locked" has inline asm
KLEE: WARNING ONCE: function "_nfs41_proc_sequence" has inline asm
KLEE: WARNING ONCE: function "nfs41_handle_sequence_flag_errors" has inline asm
KLEE: WARNING ONCE: function "nfs4_fl_copy_lock" has inline asm
KLEE: WARNING ONCE: function "rpc_pipefs_event" has inline asm
KLEE: WARNING ONCE: function "nfs4_find_client_ident" has inline asm
KLEE: WARNING ONCE: function "nfs4_callback_recallslot" has inline asm
KLEE: WARNING ONCE: function "nfs4_callback_sequence" has inline asm
KLEE: WARNING ONCE: function "rcu_read_lock___5" has inline asm
KLEE: WARNING ONCE: function "rcu_read_unlock___5" has inline asm
KLEE: WARNING ONCE: function "nfs4_delete_deviceid" has inline asm
KLEE: WARNING ONCE: function "nfs4_find_client_sessionid" has inline asm
KLEE: WARNING ONCE: function "do_callback_layoutrecall" has inline asm
KLEE: WARNING ONCE: function "nfs_async_inode_return_delegation" has inline asm
KLEE: WARNING ONCE: function "reserve_space" has inline asm
KLEE: WARNING ONCE: function "encode_attrs" has inline asm
KLEE: WARNING ONCE: function "encode_open" has inline asm
KLEE: WARNING ONCE: function "pnfs_get_layout_hdr" has inline asm
KLEE: WARNING ONCE: function "nfs_mark_delegation_referenced" has inline asm
KLEE: WARNING ONCE: function "nfs41_server_notify_highest_slotid_update" has inline asm
KLEE: WARNING ONCE: function "nfs41_server_notify_target_slotid_update" has inline asm
KLEE: WARNING ONCE: function "pnfs_layout_process" has inline asm
KLEE: WARNING ONCE: function "ldv_main2_sequence_infinite_withcheck_stateful" has inline asm
KLEE: WARNING ONCE: function "nfs_idmap_init" has inline asm
KLEE: WARNING ONCE: function "put_cred" has inline asm
KLEE: WARNING ONCE: function "nfs4_init_ds_session" has inline asm
KLEE: WARNING ONCE: function "pnfs_update_layout" has inline asm
KLEE: WARNING ONCE: function "pnfs_layout_io_set_failed" has inline asm
KLEE: WARNING ONCE: function "pnfs_ld_write_done" has inline asm
KLEE: WARNING ONCE: function "pnfs_set_layoutcommit" has inline asm
KLEE: WARNING ONCE: function "pnfs_generic_pg_writepages" has inline asm
KLEE: WARNING ONCE: function "pnfs_ld_read_done" has inline asm
KLEE: WARNING ONCE: function "pnfs_generic_pg_readpages" has inline asm
KLEE: WARNING ONCE: function "_find_get_deviceid" has inline asm
KLEE: WARNING ONCE: function "nfs4_insert_deviceid_node" has inline asm
KLEE: WARNING ONCE: function "nfs4_put_deviceid_node" has inline asm
KLEE: WARNING ONCE: function "nfs4_mark_deviceid_unavailable" has inline asm
KLEE: WARNING ONCE: function "nfs4_test_deviceid_unavailable" has inline asm
KLEE: WARNING: undefined reference to function: delayed_work_timer_fn
KLEE: WARNING: undefined reference to function: nfs_destroy_inode
KLEE: WARNING: undefined reference to function: nfs_fill_super
KLEE: WARNING: undefined reference to function: nfs_kill_super
KLEE: WARNING: undefined reference to function: nfs_put_super
KLEE: WARNING: undefined reference to function: nfs_umount_begin
KLEE: WARNING: undefined reference to variable: nfsiod_workqueue
KLEE: WARNING: undefined reference to variable: system_wq
KLEE: WARNING: undefined reference to function: user_describe
KLEE: WARNING: undefined reference to function: user_destroy
KLEE: WARNING: undefined reference to function: user_revoke
KLEE: ERROR: unable to load symbol(system_wq) while initializing globals.
Running the verifier failed
RESULT: unknown
INFO: Total time elapsed: 6.632335186
