bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--staging--lustre--lnet--lnet--lnet.ko-entry_point_true-unreach-call.cil.out.c


--------------------------------------------------------------------------------


5.0.0-KLEE:86e6f6f8-dg:03407af1-symbiotic:a8aa8ad6-minisat:3db58943-stp:17249213-sbt-instrumentation:dd7e4312
INFO: After compilation stats: Globals/Functions/Blocks/Instr.: 1012 571 7754 59589
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 1.89787912369
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'lbug_with_loc' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function libcfs_debug_msg as symbolic
Defining function libcfs_isknown_lnd as symbolic
Defining function libcfs_lnd2str as symbolic
Removed calls to 'list_del' (function is undefined)
Removed calls to 'cfs_percpt_lock' (function is undefined)
Removed calls to 'cfs_percpt_unlock' (function is undefined)
Defining function cfs_percpt_number as symbolic
Defining function cfs_cpt_current as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Defining function cfs_cpt_number as symbolic
Defining function cfs_percpt_lock_alloc as symbolic
Removed calls to 'cfs_percpt_lock_free' (function is undefined)
Removed calls to 'wait_for_completion' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to 'down' (function is undefined)
Removed calls to 'cfs_restore_sigs' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to 'vfree' (function is undefined)
Removed calls to 'cfs_percpt_free' (function is undefined)
Removed calls to 'cfs_array_free' (function is undefined)
Removed calls to '__free_pages' (function is undefined)
Defining function libcfs_nid2str as symbolic
Defining function schedule_timeout as symbolic
Defining function libcfs_id2str as symbolic
Defining function cfs_cpt_spread_node as symbolic
Defining function libcfs_net2str as symbolic
Defining function debug_lockdep_rcu_enabled as symbolic
Defining function cfs_block_allsigs as symbolic
Removed calls to 'add_wait_queue' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'remove_wait_queue' (function is undefined)
Defining function default_wake_function as symbolic
Removed calls to 'up' (function is undefined)
Defining function kthread_create_on_node as symbolic
Defining function wake_up_process as symbolic
Defining function get_seconds as symbolic
Defining function cfs_percpt_alloc as symbolic
Removed calls to 'complete' (function is undefined)
Removed calls to 'sock_release' (function is undefined)
Defining function kernel_setsockopt as symbolic
Defining function kernel_sendmsg as symbolic
Defining function kernel_recvmsg as symbolic
Defining function kernel_getpeername as symbolic
Defining function kernel_getsockname as symbolic
Defining function sock_create_lite as symbolic
Defining function kernel_listen as symbolic
Defining function sock_create as symbolic
Defining function kernel_bind as symbolic
Defining function __alloc_pages_nodemask as symbolic
Defining function libcfs_str2net as symbolic
Defining function libcfs_str2nid as symbolic
Removed calls to 'cfs_get_random_bytes' (function is undefined)
Removed calls to 'do_gettimeofday' (function is undefined)
Removed calls to 'cfs_srand' (function is undefined)
Defining function cfs_rand as symbolic
Defining function sscanf as symbolic
Defining function snprintf as symbolic
Removed calls to 'cfs_expr_list_free' (function is undefined)
Defining function libcfs_lnd2modname as symbolic
Defining function __request_module as symbolic
Defining function cfs_expr_list_parse as symbolic
Defining function cfs_trimwhite as symbolic
Defining function cfs_expr_list_values as symbolic
Removed calls to 'cfs_ip_addr_free' (function is undefined)
Defining function cfs_ip_addr_parse as symbolic
Defining function cfs_ip_addr_match as symbolic
Defining function strnlen as symbolic
Removed calls to 'fput' (function is undefined)
Defining function sock_alloc_file as symbolic
Defining function cfs_array_alloc as symbolic
Defining function cfs_cpt_weight as symbolic
Defining function ktime_get as symbolic
Removed calls to '__might_fault' (function is undefined)
Defining function _copy_to_user as symbolic
Defining function kernel_connect as symbolic
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'ldv_check_final_state' (function is undefined)
Defining function libcfs_register_ioctl as symbolic
Defining function libcfs_deregister_ioctl as symbolic
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  strchr
  strcmp
  strcpy
  strlen
  strncpy
  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: 2.31352186203
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 1080 464 4564 46043
INFO: Starting verification
KLEE: WARNING ONCE: function "lnet_init" has inline asm
KLEE: WARNING ONCE: function "LNetNIInit" has inline asm
KLEE: WARNING ONCE: function "lnet_peer_tables_create" has inline asm
KLEE: WARNING ONCE: function "lnet_res_container_setup" has inline asm
KLEE: WARNING ONCE: function "lnet_portals_create" has inline asm
KLEE: WARNING ONCE: function "lnet_unprepare" has inline asm
KLEE: WARNING ONCE: function "lnet_parse_networks" has inline asm
KLEE: WARNING ONCE: function "lnet_shutdown_lndnis" has inline asm
KLEE: WARNING ONCE: function "lnet_ni_free" has inline asm
KLEE: WARNING ONCE: function "lnet_ping_target_init" has inline asm
KLEE: WARNING ONCE: function "lnet_del_route" has inline asm
KLEE: WARNING ONCE: function "LNetEQPoll" has inline asm
KLEE: WARNING ONCE: function "LNetEQFree" has inline asm
KLEE: WARNING ONCE: function "lnet_destroy_ping_info" has inline asm
KLEE: WARNING ONCE: function "lnet_eq_free___0" has inline asm
KLEE: WARNING ONCE: function "lnet_md_free___0" has inline asm
KLEE: WARNING ONCE: function "lnet_me_free" has inline asm
KLEE: WARNING ONCE: function "LNetEQAlloc" has inline asm
KLEE: WARNING ONCE: function "lnet_router_checker" has inline asm
KLEE: WARNING ONCE: function "lnet_destroy_rc_data" has inline asm
KLEE: WARNING ONCE: function "lnet_prune_rc_data" has inline asm
KLEE: WARNING ONCE: function "fail_peer" has inline asm
KLEE: WARNING ONCE: function "lnet_msg_alloc" has inline asm
KLEE: WARNING ONCE: function "lnet_msg_free___0" has inline asm
KLEE: WARNING ONCE: function "lnet_finalize" has inline asm
KLEE: WARNING ONCE: function "lnet_msg_free" has inline asm
KLEE: WARNING ONCE: function "lnet_ni_recv" has inline asm
KLEE: WARNING ONCE: function "lnet_ni_send" has inline asm
KLEE: WARNING ONCE: function "lnet_nid2peer_locked" has inline asm
KLEE: WARNING ONCE: function "lnet_md_alloc" has inline asm
KLEE: WARNING ONCE: function "lnet_me_alloc" has inline asm
KLEE: WARNING ONCE: function "lnet_acceptor" has inline asm
KLEE: WARNING ONCE: function "lnet_sock_accept" has inline asm
KLEE: WARNING ONCE: function "lnet_rtrpool_alloc_bufs" has inline asm
KLEE: WARNING ONCE: function "lnet_rtrpool_free_bufs" has inline asm
KLEE: WARNING ONCE: function "lnet_free_text_buf" has inline asm
KLEE: WARNING ONCE: function "lnet_new_text_buf" has inline asm
KLEE: WARNING ONCE: function "lnet_add_route" has inline asm
KLEE: WARNING ONCE: function "lnet_peer_tables_cleanup" has inline asm
KLEE: WARNING ONCE: function "lnet_ni_alloc" has inline asm
KLEE: WARNING ONCE: function "lnet_fail_nid" has inline asm
KLEE: WARNING ONCE: function "lnet_res_container_cleanup" has inline asm
KLEE: WARNING ONCE: function "lnet_peer_tables_destroy" has inline asm
KLEE: WARNING ONCE: function "lnet_msg_container_cleanup" has inline asm
KLEE: WARNING ONCE: function "lnet_ptl_cleanup" has inline asm
KLEE: WARNING ONCE: function "lnet_msg_container_setup" has inline asm
KLEE: WARNING ONCE: function "lnet_notify" has inline asm
KLEE: WARNING ONCE: function "lnet_ping" has inline asm
KLEE: WARNING ONCE: function "lnet_sock_ioctl" has inline asm
KLEE: WARNING ONCE: function "lnet_ipif_enumerate" has inline asm
KLEE: WARNING ONCE: function "lnet_ipif_free_enumeration" has inline asm
KLEE: WARNING ONCE: function "lnet_copy_kiov2kiov" has inline asm
KLEE: WARNING ONCE: function "lnet_copy_kiov2iov" has inline asm
KLEE: WARNING ONCE: function "lnet_copy_iov2kiov" has inline asm
KLEE: WARNING ONCE: function "lnet_parse" has inline asm
KLEE: WARNING ONCE: function "LNetPut" has inline asm
KLEE: WARNING ONCE: function "lnet_parse_ip2nets" has inline asm
KLEE: WARNING ONCE: function "lnet_ipaddr_free_enumeration" has inline asm
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_1add631b-e13a-43ed-bfbd-e98c120d8005/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-NRTbQs/linux-4.2-rc1.tar.xz-43_2a-drivers--staging--lustre--lnet--lnet--lnet.ko-entry_point_true-unreach-call.cil.out.c:7084: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 5900 states (over memory cap)
KLEE: WARNING: killing 5936 states (over memory cap)
KLEE: WARNING: killing 6168 states (over memory cap)
KLEE: WARNING: killing 6593 states (over memory cap)
KLEE: WARNING: killing 5385 states (over memory cap)
KLEE: WARNING: killing 4973 states (over memory cap)
KLEE: WARNING: killing 5210 states (over memory cap)
KLEE: WARNING: killing 5144 states (over memory cap)
KLEE: WARNING: killing 5424 states (over memory cap)
KLEE: WARNING: killing 5364 states (over memory cap)
KLEE: WARNING: killing 5450 states (over memory cap)
KLEE: WARNING: killing 5535 states (over memory cap)
KLEE: WARNING: killing 5524 states (over memory cap)
KLEE: WARNING: killing 5654 states (over memory cap)
KLEE: WARNING: killing 5643 states (over memory cap)
KLEE: WARNING: killing 5578 states (over memory cap)
KLEE: WARNING: killing 5665 states (over memory cap)
KLEE: WARNING: killing 5893 states (over memory cap)
KLEE: WARNING: killing 5880 states (over memory cap)
KLEE: WARNING: killing 5769 states (over memory cap)
KLEE: WARNING: killing 5997 states (over memory cap)
KLEE: WARNING: killing 6078 states (over memory cap)
KLEE: WARNING: killing 6109 states (over memory cap)
KLEE: WARNING: killing 6098 states (over memory cap)
KLEE: WARNING: killing 5842 states (over memory cap)
KLEE: WARNING: killing 6013 states (over memory cap)
KLEE: WARNING: killing 6188 states (over memory cap)
KLEE: WARNING: killing 6316 states (over memory cap)
KLEE: WARNING: killing 6255 states (over memory cap)
KLEE: WARNING: killing 6234 states (over memory cap)
KLEE: WARNING: killing 6266 states (over memory cap)
KLEE: WARNING: killing 6105 states (over memory cap)
KLEE: WARNING: killing 6089 states (over memory cap)
KLEE: WARNING: killing 6256 states (over memory cap)
KLEE: WARNING: killing 6379 states (over memory cap)
KLEE: WARNING: killing 6229 states (over memory cap)
KLEE: WARNING: killing 6263 states (over memory cap)
KLEE: WARNING: killing 6243 states (over memory cap)
KLEE: WARNING: killing 6042 states (over memory cap)
KLEE: WARNING: killing 6303 states (over memory cap)
KLEE: WARNING: killing 6468 states (over memory cap)
KLEE: WARNING: killing 6361 states (over memory cap)
KLEE: WARNING: killing 6392 states (over memory cap)
KLEE: WARNING: killing 6286 states (over memory cap)
KLEE: WARNING: killing 6358 states (over memory cap)
KLEE: WARNING: killing 6119 states (over memory cap)
KLEE: WARNING: killing 6197 states (over memory cap)
KLEE: WARNING: killing 6407 states (over memory cap)
KLEE: WARNING: killing 6300 states (over memory cap)
KLEE: WARNING: killing 4508 states (over memory cap)
KLEE: WARNING: killing 6137 states (over memory cap)
KLEE: WARNING: killing 4489 states (over memory cap)
KLEE: WARNING: killing 6067 states (over memory cap)
KLEE: WARNING: killing 6233 states (over memory cap)
KLEE: WARNING: killing 4549 states (over memory cap)
KLEE: WARNING: killing 6253 states (over memory cap)
KLEE: WARNING: killing 6193 states (over memory cap)
KLEE: WARNING: killing 6083 states (over memory cap)
KLEE: WARNING: killing 4416 states (over memory cap)
KLEE: WARNING: killing 4410 states (over memory cap)
KLEE: WARNING: killing 6187 states (over memory cap)
KLEE: WARNING: killing 4396 states (over memory cap)
KLEE: WARNING: killing 6160 states (over memory cap)
KLEE: WARNING: killing 4377 states (over memory cap)
KLEE: WARNING: killing 6134 states (over memory cap)
KLEE: WARNING: killing 4359 states (over memory cap)
KLEE: WARNING: killing 6201 states (over memory cap)
KLEE: WARNING: killing 4430 states (over memory cap)
KLEE: WARNING: killing 6178 states (over memory cap)
KLEE: WARNING: killing 6119 states (over memory cap)
KLEE: WARNING: killing 4484 states (over memory cap)
KLEE: WARNING: killing 4269 states (over memory cap)
KLEE: WARNING: killing 4349 states (over memory cap)
KLEE: WARNING: killing 6040 states (over memory cap)
KLEE: WARNING: killing 4293 states (over memory cap)
KLEE: WARNING: killing 4243 states (over memory cap)
KLEE: WARNING: killing 6096 states (over memory cap)
KLEE: WARNING: killing 4398 states (over memory cap)
KLEE: WARNING: killing 6114 states (over memory cap)
KLEE: WARNING: killing 4254 states (over memory cap)
KLEE: WARNING: killing 4246 states (over memory cap)
KLEE: WARNING: killing 4197 states (over memory cap)
KLEE: WARNING: killing 4406 states (over memory cap)
KLEE: WARNING: killing 4190 states (over memory cap)
KLEE: WARNING: killing 6063 states (over memory cap)
KLEE: WARNING: killing 4387 states (over memory cap)
KLEE: WARNING: killing 4293 states (over memory cap)
KLEE: WARNING: killing 5861 states (over memory cap)
KLEE: WARNING: killing 4237 states (over memory cap)
KLEE: WARNING: killing 4395 states (over memory cap)
KLEE: WARNING: killing 6042 states (over memory cap)
KLEE: WARNING: killing 4505 states (over memory cap)
KLEE: WARNING: killing 4252 states (over memory cap)
KLEE: WARNING: killing 4244 states (over memory cap)
KLEE: WARNING: killing 4114 states (over memory cap)
KLEE: WARNING: killing 4147 states (over memory cap)
KLEE: WARNING: killing 4348 states (over memory cap)
KLEE: WARNING: killing 4138 states (over memory cap)
KLEE: WARNING: killing 4213 states (over memory cap)
