bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.12-rc1/linux-3.12-rc1.tar.xz-08_1a-fs--nfs--nfs.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.: 889 1073 10837 68756
Removed infinite loop in arch_local_save_flags
Removed infinite loop in nfs_direct_IO
Removed infinite loop in nfs_unlock_request
Removed infinite loop in arch_local_irq_restore
Removed infinite loop in arch_local_irq_disable
Removed infinite loop in nfs_fscache_release_page
Removed infinite loop in get_page
Removed infinite loop in __nfs_fscache_invalidate_page
Removed infinite loop in zero_user_segments
Removed infinite loop in zero_user_segments___0
Removed infinite loop in __nfs_readpages_from_fscache
Removed infinite loop in do_vfs_lock
Removed infinite loop in net_generic
Removed infinite loop in nfs_init_timeout_values
Removed infinite loop in ldv_stop
Removed infinite loop in nfs_atomic_open
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 2.78901004791
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_sleep' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'put_rpccred' (function is undefined)
Defining function printk as symbolic
Removed calls to 'lockdep_rcu_suspicious' (function is undefined)
Removed calls to 'dput' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'iput' (function is undefined)
Removed calls to 'mnt_set_expiry' (function is undefined)
Defining function mntget as symbolic
Defining function queue_delayed_work_on as symbolic
Removed calls to 'clear_nlink' (function is undefined)
Defining function dget_parent as symbolic
Removed calls to 'rpc_put_task_async' (function is undefined)
Defining function d_lookup as symbolic
Removed calls to '__wake_up' (function is undefined)
Defining function igrab as symbolic
Defining function rpc_run_task as symbolic
Defining function kmemdup as symbolic
Defining function is_bad_inode as symbolic
Defining function debug_lockdep_rcu_enabled as symbolic
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 '__fscache_invalidate' (function is undefined)
Removed calls to 'set_nlink' (function is undefined)
Defining function crc32_le as symbolic
Defining function check_submounts_and_drop as symbolic
Defining function security_inode_notifysecctx as symbolic
Removed calls to 'unlock_page' (function is undefined)
Removed calls to 'wake_up_bit' (function is undefined)
Defining function __set_page_dirty_nobuffers as symbolic
Removed calls to 'put_page' (function is undefined)
Removed calls to '__fscache_wait_on_page_write' (function is undefined)
Defining function generic_error_remove_page as symbolic
Defining function xs_swapper as symbolic
Defining function __page_file_mapping as symbolic
Removed calls to 'wait_on_page_bit' (function is undefined)
Defining function clear_page_dirty_for_io as symbolic
Removed calls to '__mark_inode_dirty' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Defining function out_of_line_wait_on_bit as symbolic
Defining function __refrigerator as symbolic
Defining function freezing_slow_path as symbolic
Removed calls to 'rpc_put_task' (function is undefined)
Removed calls to 'dec_zone_page_state' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to 'trace_hardirqs_off' (function is undefined)
Removed calls to '__percpu_counter_add' (function is undefined)
Removed calls to 'trace_hardirqs_on' (function is undefined)
Removed calls to 'kmem_cache_free' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Defining function _atomic_dec_and_lock as symbolic
Removed calls to 'deactivate_super' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to 'inc_zone_page_state' (function is undefined)
Defining function __rpc_wait_for_completion_task as symbolic
Defining function mempool_alloc as symbolic
Defining function __cond_resched_lock as symbolic
Defining function out_of_line_wait_on_bit_lock as symbolic
Removed calls to 'set_bdi_congested' (function is undefined)
Defining function redirty_page_for_writepage as symbolic
Removed calls to 'end_page_writeback' (function is undefined)
Removed calls to 'clear_bdi_congested' (function is undefined)
Defining function test_set_page_writeback as symbolic
Removed calls to 'io_schedule' (function is undefined)
Defining function __page_file_index as symbolic
Defining function migrate_page as symbolic
Defining function __fscache_maybe_release_page as symbolic
Removed calls to 'down_read' (function is undefined)
Removed calls to 'up_read' (function is undefined)
Removed calls to 'inode_dio_done' (function is undefined)
Defining function generic_write_checks as symbolic
Removed calls to 'unmap_mapping_range' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Defining function wait_for_completion_killable as symbolic
Defining function queue_work_on as symbolic
Defining function get_user_pages as symbolic
Defining function get_kernel_page as symbolic
Defining function __get_page_tail as symbolic
Defining function kmem_cache_alloc as symbolic
Removed calls to 'aio_complete' (function is undefined)
Removed calls to 'complete_all' (function is undefined)
Defining function sync_inode as symbolic
Removed calls to 'cancel_dirty_page' (function is undefined)
Removed calls to '__fscache_uncache_page' (function is undefined)
Defining function rpcauth_cred_key_to_expire as symbolic
Defining function grab_cache_page_write_begin as symbolic
Defining function read_cache_pages as symbolic
Defining function __fscache_read_or_alloc_pages as symbolic
Defining function write_cache_pages as symbolic
Defining function __fscache_read_or_alloc_page as symbolic
Defining function do_sync_read as symbolic
Defining function do_sync_write as symbolic
Removed calls to 'posix_test_lock' (function is undefined)
Removed calls to '__fscache_wait_on_invalidate' (function is undefined)
Defining function generic_file_splice_read as symbolic
Defining function invalidate_inode_pages2 as symbolic
Defining function generic_file_splice_write as symbolic
Defining function vfs_fsync as symbolic
Defining function posix_lock_file_wait as symbolic
Defining function flock_lock_file_wait as symbolic
Removed calls to 'prepare_to_wait' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Defining function bit_waitqueue as symbolic
Defining function wake_bit_function as symbolic
Defining function filemap_write_and_wait_range as symbolic
Defining function filemap_fdatawrite as symbolic
Removed calls to 'lockref_get' (function is undefined)
Removed calls to '__fscache_uncache_all_inode_pages' (function is undefined)
Defining function __fscache_acquire_cookie as symbolic
Removed calls to '__fscache_relinquish_cookie' (function is undefined)
Defining function rpc_lookup_cred as symbolic
Defining function generic_file_mmap as symbolic
Defining function generic_file_aio_write as symbolic
Defining function rpcauth_key_timeout_notify as symbolic
Defining function generic_file_aio_read as symbolic
Defining function generic_file_llseek as symbolic
Removed calls to 'kill_anon_super' (function is undefined)
Removed calls to 'rb_erase' (function is undefined)
Removed calls to 'synchronize_sched' (function is undefined)
Removed calls to 'rpc_shutdown_client' (function is undefined)
Removed calls to 'ida_destroy' (function is undefined)
Removed calls to 'free_percpu' (function is undefined)
Removed calls to 'bdi_destroy' (function is undefined)
Removed calls to 'idr_remove' (function is undefined)
Defining function cancel_delayed_work as symbolic
Removed calls to 'lock_acquire' (function is undefined)
Removed calls to 'lock_release' (function is undefined)
Defining function __request_module as symbolic
Removed calls to 'free_pages' (function is undefined)
Defining function kstrndup as symbolic
Defining function security_sb_copy_data as symbolic
Defining function security_sb_parse_opts_str as symbolic
Defining function match_token as symbolic
Defining function xprt_load_transport as symbolic
Defining function match_strdup as symbolic
Defining function rpc_pton as symbolic
Defining function strsep as symbolic
Defining function kstrtoull as symbolic
Defining function get_zeroed_page as symbolic
Removed calls to 'might_fault' (function is undefined)
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Defining function strndup_user as symbolic
Defining function _copy_from_user as symbolic
Defining function kstrdup as symbolic
Defining function strcat as symbolic
Defining function security_sb_set_mnt_opts as symbolic
Defining function snprintf as symbolic
Removed calls to 'bdi_unregister' (function is undefined)
Removed calls to 'deactivate_locked_super' (function is undefined)
Defining function sget as symbolic
Removed calls to 'ihold' (function is undefined)
Removed calls to 'security_d_instantiate' (function is undefined)
Removed calls to 'init_special_inode' (function is undefined)
Removed calls to 'unlock_new_inode' (function is undefined)
Defining function d_obtain_alias as symbolic
Defining function d_make_root as symbolic
Defining function iget5_locked as symbolic
Defining function make_kuid as symbolic
Defining function make_kgid as symbolic
Removed calls to 'rb_insert_color' (function is undefined)
Defining function bdi_register_dev as symbolic
Defining function set_anon_super as symbolic
Defining function security_sb_clone_mnt_opts as symbolic
Removed calls to 'call_rcu_sched' (function is undefined)
Removed calls to 'truncate_inode_pages' (function is undefined)
Removed calls to 'clear_inode' (function is undefined)
Removed calls to 'rpc_killall_tasks' (function is undefined)
Removed calls to 'rpc_print_iostats' (function is undefined)
Defining function seq_printf as symbolic
Defining function seq_puts as symbolic
Defining function find_next_bit as symbolic
Defining function rpc_peeraddr2str as symbolic
Defining function __get_free_pages as symbolic
Defining function seq_escape as symbolic
Defining function __ipv6_addr_type as symbolic
Defining function rb_first as symbolic
Defining function generic_readlink as symbolic
Removed calls to 'inode_dio_wait' (function is undefined)
Removed calls to 'generic_fillattr' (function is undefined)
Defining function filemap_write_and_wait as symbolic
Defining function read_cache_page as symbolic
Removed calls to '__pagevec_release' (function is undefined)
Defining function pagevec_lookup as symbolic
Defining function _cond_resched 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
Defining function seq_list_next as symbolic
Defining function seq_list_start_head as symbolic
Defining function filemap_fault as symbolic
Removed calls to '__lock_page' (function is undefined)
Defining function generic_file_remap_pages as symbolic
Removed calls to 'idr_destroy' (function is undefined)
Removed calls to 'idr_init' (function is undefined)
Defining function current_kernel_time as symbolic
Defining function set_page_dirty as symbolic
Defining function __fscache_write_page as symbolic
Removed calls to 'rpc_exit' (function is undefined)
Defining function rpc_restart_call_prepare as symbolic
Removed calls to 'mempool_free' (function is undefined)
Removed calls to 'mark_mounts_for_expiry' (function is undefined)
Defining function xdr_inline_decode as symbolic
Defining function xdr_reserve_space as symbolic
Defining function xdr_encode_opaque as symbolic
Defining function proc_dointvec_jiffies as symbolic
Defining function proc_dointvec as symbolic
Removed calls to 'xdr_init_decode_pages' (function is undefined)
Removed calls to 'xdr_set_scratch_buffer' (function is undefined)
Removed calls to 'kmemleak_not_leak' (function is undefined)
Defining function full_name_hash as symbolic
Defining function d_invalidate as symbolic
Defining function d_alloc as symbolic
Defining function d_materialise_unique as symbolic
Defining function alloc_pages_current as symbolic
Defining function __printk_ratelimit as symbolic
Defining function invalidate_inode_pages2_range as symbolic
Defining function autoremove_wake_function as symbolic
Defining function rpc_lookup_machine_cred as symbolic
Removed calls to '__put_net' (function is undefined)
Defining function rpc_create as symbolic
Defining function rpc_clone_client_set_auth as symbolic
Removed calls to 'rpc_setbufsize' (function is undefined)
Defining function rpc_max_payload as symbolic
Removed calls to '__list_add_rcu' (function is undefined)
Removed calls to 'ida_init' (function is undefined)
Removed calls to 'rpc_init_wait_queue' (function is undefined)
Defining function bdi_init as symbolic
Defining function __alloc_percpu as symbolic
Defining function nlmclnt_init as symbolic
Removed calls to 'nlmclnt_done' (function is undefined)
Removed calls to 'remove_proc_entry' (function is undefined)
Defining function proc_mkdir as symbolic
Defining function proc_create_data as symbolic
Removed calls to 'd_instantiate' (function is undefined)
Removed calls to 'd_drop' (function is undefined)
Removed calls to 'd_rehash' (function is undefined)
Defining function current_umask as symbolic
Defining function finish_no_open as symbolic
Defining function finish_open as symbolic
Removed calls to 'd_delete' (function is undefined)
Removed calls to '__d_drop' (function is undefined)
Defining function write_inode_now as symbolic
Removed calls to 'd_move' (function is undefined)
Defining function scnprintf as symbolic
Defining function lookup_one_len as symbolic
Removed calls to '__free_pages' (function is undefined)
Defining function add_to_page_cache_lru as symbolic
Removed calls to 'rb_replace_node' (function is undefined)
Defining function generic_permission as symbolic
Defining function ldv_release_63 as symbolic
Defining function ldv_probe_63 as symbolic
Defining function ldv_release_64 as symbolic
Defining function ldv_probe_64 as symbolic
Removed calls to 'truncate_pagecache' (function is undefined)
Defining function inode_newsize_ok as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'kmem_cache_destroy' (function is undefined)
Removed calls to 'rcu_barrier' (function is undefined)
Removed calls to '__fscache_unregister_netfs' (function is undefined)
Removed calls to 'unregister_pernet_subsys' (function is undefined)
Removed calls to 'rpc_proc_unregister' (function is undefined)
Removed calls to 'destroy_workqueue' (function is undefined)
Removed calls to 'page_put_link' (function is undefined)
Removed calls to 'delayed_work_timer_fn' (function is undefined)
Defining function ftrace_event_reg as symbolic
Defining function trace_event_raw_init as symbolic
Defining function trace_define_field as symbolic
Defining function param_get_uint as symbolic
Defining function ftrace_raw_output_prep as symbolic
Defining function trace_seq_printf as symbolic
Defining function register_pernet_subsys as symbolic
Removed calls to 'mempool_destroy' (function is undefined)
Defining function rpc_proc_register as symbolic
Defining function register_filesystem as symbolic
Defining function register_shrinker as symbolic
Defining function unregister_filesystem as symbolic
Defining function register_sysctl_table as symbolic
Defining function kmem_cache_create as symbolic
Defining function int_sqrt as symbolic
Defining function mempool_alloc_slab as symbolic
Defining function mempool_create as symbolic
Removed calls to 'inode_init_once' (function is undefined)
Removed calls to '__init_rwsem' (function is undefined)
Defining function __alloc_workqueue_key as symbolic
Defining function __fscache_register_netfs as symbolic
Removed calls to 'unregister_shrinker' (function is undefined)
Removed calls to 'unregister_sysctl_table' (function is undefined)
Defining function ftrace_print_flags_seq as symbolic
Defining function ldv_release_56 as symbolic
Defining function ldv_probe_56 as symbolic
Defining function ldv_release_55 as symbolic
Defining function ldv_probe_55 as symbolic
Defining function ldv_release_44 as symbolic
Defining function ldv_probe_44 as symbolic
Defining function ftrace_print_symbols_seq as symbolic
Defining function rpcauth_get_gssinfo as symbolic
Defining function rpc_call_sync as symbolic
Defining function vfs_kern_mount as symbolic
Linked our definitions to these undefined functions:
  memcmp
  strchr
  strcpy
  strlen
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_assume
  __VERIFIER_calloc0
  __VERIFIER_error
  __VERIFIER_exit
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
  __VERIFIER_nondet_loff_t_named
  __VERIFIER_nondet_pointer_named
  __VERIFIER_nondet_size_t_named
  __VERIFIER_nondet_uint_named
  __VERIFIER_nondet_ulong_named
INFO: After-slicing optimizations and preparation time: 2.76497983932
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 1339 737 5709 40056
INFO: Starting verification
KLEE: WARNING ONCE: function "nfs_readdir" has inline asm
KLEE: WARNING ONCE: function "nfs_opendir" has inline asm
KLEE: WARNING ONCE: function "nfs_fsync_dir" has inline asm
KLEE: WARNING ONCE: function "nfs_readdir_clear_array" has inline asm
KLEE: WARNING ONCE: function "nfs_lookup_revalidate" has inline asm
KLEE: WARNING ONCE: function "nfs_alloc_fattr" has inline asm
KLEE: WARNING ONCE: function "nfs_complete_unlink" has inline asm
KLEE: WARNING ONCE: function "nfs_do_call_unlink" has inline asm
KLEE: WARNING ONCE: function "nfs_dec_sillycount" has inline asm
KLEE: WARNING ONCE: function "__nfs_revalidate_inode" has inline asm
KLEE: WARNING ONCE: function "rcu_read_lock_sched_held" has inline asm
KLEE: WARNING ONCE: function "nfs_zap_caches_locked" has inline asm
KLEE: WARNING ONCE: function "nfs_refresh_inode_locked" has inline asm
KLEE: WARNING ONCE: function "arch_local_save_flags" has inline asm
KLEE: WARNING ONCE: function "nfs_readpage" has inline asm
KLEE: WARNING ONCE: function "nfs_writepages" has inline asm
KLEE: WARNING ONCE: function "nfs_readpages" has inline asm
KLEE: WARNING ONCE: function "nfs_write_begin" has inline asm
KLEE: WARNING ONCE: function "nfs_write_end" has inline asm
KLEE: WARNING ONCE: function "nfs_release_page" has inline asm
KLEE: WARNING ONCE: function "nfs_direct_IO" has inline asm
KLEE: WARNING ONCE: function "nfs_wb_page" has inline asm
KLEE: WARNING ONCE: function "nfs_commit_inode" has inline asm
KLEE: WARNING ONCE: function "nfs_wait_bit_killable" has inline asm
KLEE: WARNING ONCE: function "nfs_generic_commit_list" has inline asm
KLEE: WARNING ONCE: function "nfs_init_commit" has inline asm
KLEE: WARNING ONCE: function "dec_bdi_stat" has inline asm
KLEE: WARNING ONCE: function "nfs_unlock_request" has inline asm
KLEE: WARNING ONCE: function "nfs_release_request" has inline asm
KLEE: WARNING ONCE: function "nfs_request_add_commit_list" has inline asm
KLEE: WARNING ONCE: function "arch_local_irq_save" has inline asm
KLEE: WARNING ONCE: function "arch_local_irq_restore" has inline asm
KLEE: WARNING ONCE: function "nfs_clear_request" has inline asm
KLEE: WARNING ONCE: function "__put_nfs_open_context" has inline asm
KLEE: WARNING ONCE: function "nfs_sb_deactive" has inline asm
KLEE: WARNING ONCE: function "_nfs4_state_protect" has inline asm
KLEE: WARNING ONCE: function "nfs_scan_commit_list" has inline asm
KLEE: WARNING ONCE: function "kref_get" has inline asm
KLEE: WARNING ONCE: function "nfs_request_remove_commit_list" has inline asm
KLEE: WARNING ONCE: function "nfs_do_writepage" has inline asm
KLEE: WARNING ONCE: function "nfs_wait_on_request" has inline asm
KLEE: WARNING ONCE: function "nfs_end_page_writeback" has inline asm
KLEE: WARNING ONCE: function "nfs_fscache_release_page" has inline asm
KLEE: WARNING ONCE: function "nfs_file_direct_read" has inline asm
KLEE: WARNING ONCE: function "nfs_file_direct_write" has inline asm
KLEE: WARNING ONCE: function "nfs_get_lock_context" has inline asm
KLEE: WARNING ONCE: function "nfs_create_request" has inline asm
KLEE: WARNING ONCE: function "nfs_direct_req_release" has inline asm
KLEE: WARNING ONCE: function "__nfs_find_lock_context" has inline asm
KLEE: WARNING ONCE: function "nfs_direct_write_reschedule" has inline asm
KLEE: WARNING ONCE: function "nfs_wb_all" has inline asm
KLEE: WARNING ONCE: function "nfs_wb_page_cancel" has inline asm
KLEE: WARNING ONCE: function "__nfs_fscache_invalidate_page" has inline asm
KLEE: WARNING ONCE: function "nfs_inode_remove_request" has inline asm
KLEE: WARNING ONCE: function "zero_user_segments" has inline asm
KLEE: WARNING ONCE: function "nfs_updatepage" has inline asm
KLEE: WARNING ONCE: function "nfs_flush_incompatible" has inline asm
KLEE: WARNING ONCE: function "nfs_find_open_context" has inline asm
KLEE: WARNING ONCE: function "__nfs_readpages_from_fscache" has inline asm
KLEE: WARNING ONCE: function "readpage_async_filler" has inline asm
KLEE: WARNING ONCE: function "zero_user_segment___0" has inline asm
KLEE: WARNING ONCE: function "nfs_readpage_from_fscache_complete" has inline asm
KLEE: WARNING ONCE: function "nfs_readpage_async" has inline asm
KLEE: WARNING ONCE: function "__nfs_readpage_from_fscache" has inline asm
KLEE: WARNING ONCE: function "nfs_file_read" has inline asm
KLEE: WARNING ONCE: function "nfs_file_write" has inline asm
KLEE: WARNING ONCE: function "nfs_file_open" has inline asm
KLEE: WARNING ONCE: function "nfs_file_flush" has inline asm
KLEE: WARNING ONCE: function "nfs_file_release" has inline asm
KLEE: WARNING ONCE: function "nfs_file_fsync" has inline asm
KLEE: WARNING ONCE: function "nfs_lock" has inline asm
KLEE: WARNING ONCE: function "nfs_file_splice_write" has inline asm
KLEE: WARNING ONCE: function "nfs_file_splice_read" has inline asm
KLEE: WARNING ONCE: function "nfs_revalidate_mapping" has inline asm
KLEE: WARNING ONCE: function "do_vfs_lock" has inline asm
KLEE: WARNING ONCE: function "nfs_iocounter_wait" has inline asm
KLEE: WARNING ONCE: function "nfs_file_fsync_commit" has inline asm
KLEE: WARNING ONCE: function "alloc_nfs_open_context" has inline asm
KLEE: WARNING ONCE: function "nfs_file_set_open_context" has inline asm
KLEE: WARNING ONCE: function "nfs_fscache_set_inode_cookie" has inline asm
KLEE: WARNING ONCE: function "nfs_fscache_inode_lock" has inline asm
KLEE: WARNING ONCE: function "nfs_fs_mount" has inline asm
KLEE: WARNING ONCE: function "nfs_free_server" has inline asm
KLEE: WARNING ONCE: function "net_generic" 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_fhget" has inline asm
KLEE: WARNING ONCE: function "nfs_show_stats" has inline asm
KLEE: WARNING ONCE: function "nfs_path" has inline asm
KLEE: WARNING ONCE: function "nfs_access_zap_cache" has inline asm
KLEE: WARNING ONCE: function "nfs_access_free_list" has inline asm
KLEE: WARNING ONCE: function "nfs_setattr" has inline asm
KLEE: WARNING ONCE: function "nfs_getattr" has inline asm
KLEE: WARNING ONCE: function "nfs_symlink_filler" has inline asm
KLEE: WARNING ONCE: function "nfs_fh_get_context" has inline asm
KLEE: WARNING ONCE: function "nfs_fscache_inode_now_uncached" has inline asm
KLEE: WARNING ONCE: function "nfs_vm_page_mkwrite" has inline asm
KLEE: WARNING ONCE: function "nfs_access_cache_scan" has inline asm
KLEE: WARNING ONCE: function "nfs_direct_commit_complete" has inline asm
KLEE: WARNING ONCE: function "nfs_direct_pgio_init" has inline asm
KLEE: WARNING ONCE: function "nfs_direct_write_completion" has inline asm
KLEE: WARNING ONCE: function "nfs_direct_read_completion" has inline asm
KLEE: WARNING ONCE: function "nfs_read_completion" has inline asm
KLEE: WARNING ONCE: function "__nfs_readpage_to_fscache" has inline asm
KLEE: WARNING ONCE: function "nfs_readpage_result_common" has inline asm
KLEE: WARNING ONCE: function "nfs_readdata_release" has inline asm
KLEE: WARNING ONCE: function "nfs_readpage_result" has inline asm
KLEE: WARNING ONCE: function "nfs_set_pgio_error" has inline asm
KLEE: WARNING ONCE: function "nfs_generic_pg_readpages" has inline asm
KLEE: WARNING ONCE: function "nfs_readdata_alloc" has inline asm
KLEE: WARNING ONCE: function "nfs_pagein_error" has inline asm
KLEE: WARNING ONCE: function "nfs_read_rpcsetup" has inline asm
KLEE: WARNING ONCE: function "nfs_async_unlink_done" has inline asm
KLEE: WARNING ONCE: function "nfs_async_rename_done" has inline asm
KLEE: WARNING ONCE: function "nfs_commit_clear_lock" has inline asm
KLEE: WARNING ONCE: function "nfs_commit_release_pages" has inline asm
KLEE: WARNING ONCE: function "nfs_write_completion" has inline asm
KLEE: WARNING ONCE: function "nfs_writeback_release_common" has inline asm
KLEE: WARNING ONCE: function "nfs_writedata_release" has inline asm
KLEE: WARNING ONCE: function "nfs_writeback_done" has inline asm
KLEE: WARNING ONCE: function "nfs_generic_pg_writepages" has inline asm
KLEE: WARNING ONCE: function "nfs_writedata_alloc" has inline asm
KLEE: WARNING ONCE: function "nfs_flush_error" has inline asm
KLEE: WARNING ONCE: function "nfs_write_rpcsetup" has inline asm
KLEE: WARNING ONCE: function "nfs_block_sillyrename" has inline asm
KLEE: WARNING ONCE: function "nfs_readdir_filler" has inline asm
KLEE: WARNING ONCE: function "nfs_readdir_xdr_to_array" has inline asm
KLEE: WARNING ONCE: function "nfs_unblock_sillyrename" has inline asm
KLEE: WARNING ONCE: function "nfs_fattr_init" has inline asm
KLEE: WARNING ONCE: function "nfs_inc_attr_generation_counter" has inline asm
KLEE: WARNING ONCE: function "nfs_sb_active" has inline asm
KLEE: WARNING ONCE: function "get_nfs_open_context" has inline asm
KLEE: WARNING ONCE: function "nfs_fscache_init_inode_cookie" has inline asm
KLEE: WARNING ONCE: function "nfs_alloc_client" has inline asm
KLEE: WARNING ONCE: function "nfs_free_client" has inline asm
KLEE: WARNING ONCE: function "nfs_wait_client_init_complete" has inline asm
KLEE: WARNING ONCE: function "nfs_get_client" has inline asm
KLEE: WARNING ONCE: function "nfs_init_timeout_values" has inline asm
KLEE: WARNING ONCE: function "nfs_probe_fsinfo" has inline asm
KLEE: WARNING ONCE: function "nfs_server_insert_lists" has inline asm
KLEE: WARNING ONCE: function "nfs_create_server" has inline asm
KLEE: WARNING ONCE: function "nfs_clone_server" has inline asm
KLEE: WARNING ONCE: function "nfs_lookup" has inline asm
KLEE: WARNING ONCE: function "nfs_atomic_open" has inline asm
KLEE: WARNING ONCE: function "trace_nfs_atomic_open_exit" has inline asm
KLEE: WARNING ONCE: function "nfs_create" has inline asm
KLEE: WARNING ONCE: function "nfs_mknod" has inline asm
KLEE: WARNING ONCE: function "nfs_mkdir" has inline asm
KLEE: WARNING ONCE: function "nfs_rmdir" has inline asm
KLEE: WARNING ONCE: function "nfs_wait_on_sillyrename" has inline asm
KLEE: WARNING ONCE: function "nfs_unlink" has inline asm
KLEE: WARNING ONCE: function "nfs_sillyrename" has inline asm
KLEE: WARNING ONCE: function "nfs_symlink" has inline asm
KLEE: WARNING ONCE: function "nfs_link" has inline asm
KLEE: WARNING ONCE: function "nfs_rename" has inline asm
KLEE: WARNING ONCE: function "nfs_access_add_cache" has inline asm
KLEE: WARNING ONCE: function "nfs_do_access" has inline asm
KLEE: WARNING ONCE: function "nfs_permission" has inline asm
KLEE: WARNING ONCE: function "nfs_setattr_update_inode" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_48" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_50" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_1" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_37" has inline asm
KLEE: WARNING ONCE: function "nfs_fscache_reset_inode_cookie" has inline asm
KLEE: WARNING: undefined reference to variable: boot_tvec_bases
KLEE: WARNING: undefined reference to function: delayed_work_timer_fn
KLEE: WARNING: undefined reference to variable: init_user_ns
KLEE: WARNING: undefined reference to function: mempool_free_slab
KLEE: WARNING: undefined reference to function: page_put_link
KLEE: WARNING: undefined reference to variable: system_wq
KLEE: ERROR: unable to load symbol(system_wq) while initializing globals.
KLEE: output directory is "/tmp/symbiotic-j5vfMC/klee-out-0"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: function "nfs_readdir" has inline asm
KLEE: WARNING ONCE: function "nfs_opendir" has inline asm
KLEE: WARNING ONCE: function "nfs_fsync_dir" has inline asm
KLEE: WARNING ONCE: function "nfs_readdir_clear_array" has inline asm
KLEE: WARNING ONCE: function "nfs_lookup_revalidate" has inline asm
KLEE: WARNING ONCE: function "nfs_alloc_fattr" has inline asm
KLEE: WARNING ONCE: function "nfs_complete_unlink" has inline asm
KLEE: WARNING ONCE: function "nfs_do_call_unlink" has inline asm
KLEE: WARNING ONCE: function "nfs_dec_sillycount" has inline asm
KLEE: WARNING ONCE: function "__nfs_revalidate_inode" has inline asm
KLEE: WARNING ONCE: function "rcu_read_lock_sched_held" has inline asm
KLEE: WARNING ONCE: function "nfs_zap_caches_locked" has inline asm
KLEE: WARNING ONCE: function "nfs_refresh_inode_locked" has inline asm
KLEE: WARNING ONCE: function "arch_local_save_flags" has inline asm
KLEE: WARNING ONCE: function "nfs_readpage" has inline asm
KLEE: WARNING ONCE: function "nfs_writepages" has inline asm
KLEE: WARNING ONCE: function "nfs_readpages" has inline asm
KLEE: WARNING ONCE: function "nfs_write_begin" has inline asm
KLEE: WARNING ONCE: function "nfs_write_end" has inline asm
KLEE: WARNING ONCE: function "nfs_release_page" has inline asm
KLEE: WARNING ONCE: function "nfs_direct_IO" has inline asm
KLEE: WARNING ONCE: function "nfs_wb_page" has inline asm
KLEE: WARNING ONCE: function "nfs_commit_inode" has inline asm
KLEE: WARNING ONCE: function "nfs_wait_bit_killable" has inline asm
KLEE: WARNING ONCE: function "nfs_generic_commit_list" has inline asm
KLEE: WARNING ONCE: function "nfs_init_commit" has inline asm
KLEE: WARNING ONCE: function "dec_bdi_stat" has inline asm
KLEE: WARNING ONCE: function "nfs_unlock_request" has inline asm
KLEE: WARNING ONCE: function "nfs_release_request" has inline asm
KLEE: WARNING ONCE: function "nfs_request_add_commit_list" has inline asm
KLEE: WARNING ONCE: function "arch_local_irq_save" has inline asm
KLEE: WARNING ONCE: function "arch_local_irq_restore" has inline asm
KLEE: WARNING ONCE: function "nfs_clear_request" has inline asm
KLEE: WARNING ONCE: function "__put_nfs_open_context" has inline asm
KLEE: WARNING ONCE: function "nfs_sb_deactive" has inline asm
KLEE: WARNING ONCE: function "_nfs4_state_protect" has inline asm
KLEE: WARNING ONCE: function "nfs_scan_commit_list" has inline asm
KLEE: WARNING ONCE: function "kref_get" has inline asm
KLEE: WARNING ONCE: function "nfs_request_remove_commit_list" has inline asm
KLEE: WARNING ONCE: function "nfs_do_writepage" has inline asm
KLEE: WARNING ONCE: function "nfs_wait_on_request" has inline asm
KLEE: WARNING ONCE: function "nfs_end_page_writeback" has inline asm
KLEE: WARNING ONCE: function "nfs_fscache_release_page" has inline asm
KLEE: WARNING ONCE: function "nfs_file_direct_read" has inline asm
KLEE: WARNING ONCE: function "nfs_file_direct_write" has inline asm
KLEE: WARNING ONCE: function "nfs_get_lock_context" has inline asm
KLEE: WARNING ONCE: function "nfs_create_request" has inline asm
KLEE: WARNING ONCE: function "nfs_direct_req_release" has inline asm
KLEE: WARNING ONCE: function "__nfs_find_lock_context" has inline asm
KLEE: WARNING ONCE: function "nfs_direct_write_reschedule" has inline asm
KLEE: WARNING ONCE: function "nfs_wb_all" has inline asm
KLEE: WARNING ONCE: function "nfs_wb_page_cancel" has inline asm
KLEE: WARNING ONCE: function "__nfs_fscache_invalidate_page" has inline asm
KLEE: WARNING ONCE: function "nfs_inode_remove_request" has inline asm
KLEE: WARNING ONCE: function "zero_user_segments" has inline asm
KLEE: WARNING ONCE: function "nfs_updatepage" has inline asm
KLEE: WARNING ONCE: function "nfs_flush_incompatible" has inline asm
KLEE: WARNING ONCE: function "nfs_find_open_context" has inline asm
KLEE: WARNING ONCE: function "__nfs_readpages_from_fscache" has inline asm
KLEE: WARNING ONCE: function "readpage_async_filler" has inline asm
KLEE: WARNING ONCE: function "zero_user_segment___0" has inline asm
KLEE: WARNING ONCE: function "nfs_readpage_from_fscache_complete" has inline asm
KLEE: WARNING ONCE: function "nfs_readpage_async" has inline asm
KLEE: WARNING ONCE: function "__nfs_readpage_from_fscache" has inline asm
KLEE: WARNING ONCE: function "nfs_file_read" has inline asm
KLEE: WARNING ONCE: function "nfs_file_write" has inline asm
KLEE: WARNING ONCE: function "nfs_file_open" has inline asm
KLEE: WARNING ONCE: function "nfs_file_flush" has inline asm
KLEE: WARNING ONCE: function "nfs_file_release" has inline asm
KLEE: WARNING ONCE: function "nfs_file_fsync" has inline asm
KLEE: WARNING ONCE: function "nfs_lock" has inline asm
KLEE: WARNING ONCE: function "nfs_file_splice_write" has inline asm
KLEE: WARNING ONCE: function "nfs_file_splice_read" has inline asm
KLEE: WARNING ONCE: function "nfs_revalidate_mapping" has inline asm
KLEE: WARNING ONCE: function "do_vfs_lock" has inline asm
KLEE: WARNING ONCE: function "nfs_iocounter_wait" has inline asm
KLEE: WARNING ONCE: function "nfs_file_fsync_commit" has inline asm
KLEE: WARNING ONCE: function "alloc_nfs_open_context" has inline asm
KLEE: WARNING ONCE: function "nfs_file_set_open_context" has inline asm
KLEE: WARNING ONCE: function "nfs_fscache_set_inode_cookie" has inline asm
KLEE: WARNING ONCE: function "nfs_fscache_inode_lock" has inline asm
KLEE: WARNING ONCE: function "nfs_fs_mount" has inline asm
KLEE: WARNING ONCE: function "nfs_free_server" has inline asm
KLEE: WARNING ONCE: function "net_generic" 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_fhget" has inline asm
KLEE: WARNING ONCE: function "nfs_show_stats" has inline asm
KLEE: WARNING ONCE: function "nfs_path" has inline asm
KLEE: WARNING ONCE: function "nfs_access_zap_cache" has inline asm
KLEE: WARNING ONCE: function "nfs_access_free_list" has inline asm
KLEE: WARNING ONCE: function "nfs_setattr" has inline asm
KLEE: WARNING ONCE: function "nfs_getattr" has inline asm
KLEE: WARNING ONCE: function "nfs_symlink_filler" has inline asm
KLEE: WARNING ONCE: function "nfs_fh_get_context" has inline asm
KLEE: WARNING ONCE: function "nfs_fscache_inode_now_uncached" has inline asm
KLEE: WARNING ONCE: function "nfs_vm_page_mkwrite" has inline asm
KLEE: WARNING ONCE: function "nfs_access_cache_scan" has inline asm
KLEE: WARNING ONCE: function "nfs_direct_commit_complete" has inline asm
KLEE: WARNING ONCE: function "nfs_direct_pgio_init" has inline asm
KLEE: WARNING ONCE: function "nfs_direct_write_completion" has inline asm
KLEE: WARNING ONCE: function "nfs_direct_read_completion" has inline asm
KLEE: WARNING ONCE: function "nfs_read_completion" has inline asm
KLEE: WARNING ONCE: function "__nfs_readpage_to_fscache" has inline asm
KLEE: WARNING ONCE: function "nfs_readpage_result_common" has inline asm
KLEE: WARNING ONCE: function "nfs_readdata_release" has inline asm
KLEE: WARNING ONCE: function "nfs_readpage_result" has inline asm
KLEE: WARNING ONCE: function "nfs_set_pgio_error" has inline asm
KLEE: WARNING ONCE: function "nfs_generic_pg_readpages" has inline asm
KLEE: WARNING ONCE: function "nfs_readdata_alloc" has inline asm
KLEE: WARNING ONCE: function "nfs_pagein_error" has inline asm
KLEE: WARNING ONCE: function "nfs_read_rpcsetup" has inline asm
KLEE: WARNING ONCE: function "nfs_async_unlink_done" has inline asm
KLEE: WARNING ONCE: function "nfs_async_rename_done" has inline asm
KLEE: WARNING ONCE: function "nfs_commit_clear_lock" has inline asm
KLEE: WARNING ONCE: function "nfs_commit_release_pages" has inline asm
KLEE: WARNING ONCE: function "nfs_write_completion" has inline asm
KLEE: WARNING ONCE: function "nfs_writeback_release_common" has inline asm
KLEE: WARNING ONCE: function "nfs_writedata_release" has inline asm
KLEE: WARNING ONCE: function "nfs_writeback_done" has inline asm
KLEE: WARNING ONCE: function "nfs_generic_pg_writepages" has inline asm
KLEE: WARNING ONCE: function "nfs_writedata_alloc" has inline asm
KLEE: WARNING ONCE: function "nfs_flush_error" has inline asm
KLEE: WARNING ONCE: function "nfs_write_rpcsetup" has inline asm
KLEE: WARNING ONCE: function "nfs_block_sillyrename" has inline asm
KLEE: WARNING ONCE: function "nfs_readdir_filler" has inline asm
KLEE: WARNING ONCE: function "nfs_readdir_xdr_to_array" has inline asm
KLEE: WARNING ONCE: function "nfs_unblock_sillyrename" has inline asm
KLEE: WARNING ONCE: function "nfs_fattr_init" has inline asm
KLEE: WARNING ONCE: function "nfs_inc_attr_generation_counter" has inline asm
KLEE: WARNING ONCE: function "nfs_sb_active" has inline asm
KLEE: WARNING ONCE: function "get_nfs_open_context" has inline asm
KLEE: WARNING ONCE: function "nfs_fscache_init_inode_cookie" has inline asm
KLEE: WARNING ONCE: function "nfs_alloc_client" has inline asm
KLEE: WARNING ONCE: function "nfs_free_client" has inline asm
KLEE: WARNING ONCE: function "nfs_wait_client_init_complete" has inline asm
KLEE: WARNING ONCE: function "nfs_get_client" has inline asm
KLEE: WARNING ONCE: function "nfs_init_timeout_values" has inline asm
KLEE: WARNING ONCE: function "nfs_probe_fsinfo" has inline asm
KLEE: WARNING ONCE: function "nfs_server_insert_lists" has inline asm
KLEE: WARNING ONCE: function "nfs_create_server" has inline asm
KLEE: WARNING ONCE: function "nfs_clone_server" has inline asm
KLEE: WARNING ONCE: function "nfs_lookup" has inline asm
KLEE: WARNING ONCE: function "nfs_atomic_open" has inline asm
KLEE: WARNING ONCE: function "trace_nfs_atomic_open_exit" has inline asm
KLEE: WARNING ONCE: function "nfs_create" has inline asm
KLEE: WARNING ONCE: function "nfs_mknod" has inline asm
KLEE: WARNING ONCE: function "nfs_mkdir" has inline asm
KLEE: WARNING ONCE: function "nfs_rmdir" has inline asm
KLEE: WARNING ONCE: function "nfs_wait_on_sillyrename" has inline asm
KLEE: WARNING ONCE: function "nfs_unlink" has inline asm
KLEE: WARNING ONCE: function "nfs_sillyrename" has inline asm
KLEE: WARNING ONCE: function "nfs_symlink" has inline asm
KLEE: WARNING ONCE: function "nfs_link" has inline asm
KLEE: WARNING ONCE: function "nfs_rename" has inline asm
KLEE: WARNING ONCE: function "nfs_access_add_cache" has inline asm
KLEE: WARNING ONCE: function "nfs_do_access" has inline asm
KLEE: WARNING ONCE: function "nfs_permission" has inline asm
KLEE: WARNING ONCE: function "nfs_setattr_update_inode" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_48" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_50" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_1" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_37" has inline asm
KLEE: WARNING ONCE: function "nfs_fscache_reset_inode_cookie" has inline asm
KLEE: WARNING: undefined reference to variable: boot_tvec_bases
KLEE: WARNING: undefined reference to function: delayed_work_timer_fn
KLEE: WARNING: undefined reference to variable: init_user_ns
KLEE: WARNING: undefined reference to function: mempool_free_slab
KLEE: WARNING: undefined reference to function: page_put_link
KLEE: WARNING: undefined reference to variable: system_wq
KLEE: ERROR: unable to load symbol(system_wq) while initializing globals.
Running the verifier failed
RESULT: unknown
INFO: Total time elapsed: 6.37697386742
