bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-32_7a-drivers--staging--lustre--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.: 1017 577 7986 58669
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 1.8875348568
Removed calls to 'lbug_with_loc' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to 'mutex_lock' (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 'mutex_unlock' (function is undefined)
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 __kmalloc_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 vmalloc 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 vmalloc_node 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)
Defining function mutex_trylock as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Defining function libcfs_register_ioctl as symbolic
Defining function libcfs_deregister_ioctl as symbolic
Linked our definitions to these undefined functions:
  strchr
  strcmp
  strcpy
  strlen
  strncpy
  __kmalloc
  kfree
  __VERIFIER_assume
  __VERIFIER_calloc0
  __VERIFIER_error
  __VERIFIER_exit
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
  __VERIFIER_nondet_pointer_named
  __VERIFIER_nondet_ulong_named
INFO: After-slicing optimizations and preparation time: 2.27470612526
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 1085 473 4618 44831
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" has inline asm
KLEE: WARNING ONCE: function "lnet_finalize" 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_ab7af83b-c112-4c1d-85fb-d5202a326fe9/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-rumsir/linux-4.2-rc1.tar.xz-32_7a-drivers--staging--lustre--lnet--lnet--lnet.ko-entry_point_true-unreach-call.cil.out.c:7053: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 5597 states (over memory cap)
KLEE: WARNING: killing 5885 states (over memory cap)
KLEE: WARNING: killing 6117 states (over memory cap)
KLEE: WARNING: killing 5205 states (over memory cap)
KLEE: WARNING: killing 5042 states (over memory cap)
KLEE: WARNING: killing 5177 states (over memory cap)
KLEE: WARNING: killing 5015 states (over memory cap)
KLEE: WARNING: killing 5251 states (over memory cap)
KLEE: WARNING: killing 5289 states (over memory cap)
KLEE: WARNING: killing 5522 states (over memory cap)
KLEE: WARNING: killing 5407 states (over memory cap)
KLEE: WARNING: killing 5491 states (over memory cap)
KLEE: WARNING: killing 5673 states (over memory cap)
KLEE: WARNING: killing 5511 states (over memory cap)
KLEE: WARNING: killing 5598 states (over memory cap)
KLEE: WARNING: killing 5533 states (over memory cap)
KLEE: WARNING: killing 5764 states (over memory cap)
KLEE: WARNING: killing 5656 states (over memory cap)
KLEE: WARNING: killing 5886 states (over memory cap)
KLEE: WARNING: killing 5872 states (over memory cap)
KLEE: WARNING: killing 6002 states (over memory cap)
KLEE: WARNING: killing 5989 states (over memory cap)
KLEE: WARNING: killing 5923 states (over memory cap)
KLEE: WARNING: killing 6050 states (over memory cap)
KLEE: WARNING: killing 6232 states (over memory cap)
KLEE: WARNING: killing 5975 states (over memory cap)
KLEE: WARNING: killing 6007 states (over memory cap)
KLEE: WARNING: killing 5991 states (over memory cap)
KLEE: WARNING: killing 6356 states (over memory cap)
KLEE: WARNING: killing 6293 states (over memory cap)
KLEE: WARNING: killing 6137 states (over memory cap)
KLEE: WARNING: killing 6219 states (over memory cap)
KLEE: WARNING: killing 6155 states (over memory cap)
KLEE: WARNING: killing 6185 states (over memory cap)
KLEE: WARNING: killing 6121 states (over memory cap)
KLEE: WARNING: killing 6384 states (over memory cap)
KLEE: WARNING: killing 6133 states (over memory cap)
KLEE: WARNING: killing 6396 states (over memory cap)
KLEE: WARNING: killing 6425 states (over memory cap)
KLEE: WARNING: killing 6175 states (over memory cap)
KLEE: WARNING: killing 6296 states (over memory cap)
KLEE: WARNING: killing 6098 states (over memory cap)
KLEE: WARNING: killing 6357 states (over memory cap)
KLEE: WARNING: killing 6345 states (over memory cap)
KLEE: WARNING: killing 6418 states (over memory cap)
KLEE: WARNING: killing 4565 states (over memory cap)
KLEE: WARNING: killing 6124 states (over memory cap)
KLEE: WARNING: killing 6331 states (over memory cap)
KLEE: WARNING: killing 4487 states (over memory cap)
KLEE: WARNING: killing 6176 states (over memory cap)
KLEE: WARNING: killing 6161 states (over memory cap)
KLEE: WARNING: killing 6279 states (over memory cap)
KLEE: WARNING: killing 4540 states (over memory cap)
KLEE: WARNING: killing 6215 states (over memory cap)
KLEE: WARNING: killing 4568 states (over memory cap)
KLEE: WARNING: killing 6234 states (over memory cap)
KLEE: WARNING: killing 4460 states (over memory cap)
KLEE: WARNING: killing 6249 states (over memory cap)
KLEE: WARNING: killing 4533 states (over memory cap)
KLEE: WARNING: killing 6052 states (over memory cap)
KLEE: WARNING: killing 4384 states (over memory cap)
KLEE: WARNING: killing 4463 states (over memory cap)
KLEE: WARNING: killing 6108 states (over memory cap)
KLEE: WARNING: killing 4449 states (over memory cap)
KLEE: WARNING: killing 6089 states (over memory cap)
KLEE: WARNING: killing 4388 states (over memory cap)
KLEE: WARNING: killing 6191 states (over memory cap)
KLEE: WARNING: killing 4457 states (over memory cap)
KLEE: WARNING: killing 4455 states (over memory cap)
KLEE: WARNING: killing 4360 states (over memory cap)
KLEE: WARNING: killing 6109 states (over memory cap)
KLEE: WARNING: killing 4299 states (over memory cap)
KLEE: WARNING: killing 4289 states (over memory cap)
KLEE: WARNING: killing 4412 states (over memory cap)
KLEE: WARNING: killing 4320 states (over memory cap)
KLEE: WARNING: killing 4358 states (over memory cap)
KLEE: WARNING: killing 4307 states (over memory cap)
KLEE: WARNING: killing 6169 states (over memory cap)
KLEE: WARNING: killing 4419 states (over memory cap)
KLEE: WARNING: killing 6056 states (over memory cap)
KLEE: WARNING: killing 4525 states (over memory cap)
KLEE: WARNING: killing 4394 states (over memory cap)
KLEE: WARNING: killing 4260 states (over memory cap)
KLEE: WARNING: killing 4294 states (over memory cap)
KLEE: WARNING: killing 4290 states (over memory cap)
KLEE: WARNING: killing 4197 states (over memory cap)
KLEE: WARNING: killing 4362 states (over memory cap)
KLEE: WARNING: killing 4273 states (over memory cap)
KLEE: WARNING: killing 4224 states (over memory cap)
KLEE: WARNING: killing 4260 states (over memory cap)
KLEE: WARNING: killing 6121 states (over memory cap)
KLEE: WARNING: killing 4451 states (over memory cap)
KLEE: WARNING: killing 4280 states (over memory cap)
KLEE: WARNING: killing 4194 states (over memory cap)
KLEE: WARNING: killing 4395 states (over memory cap)
KLEE: WARNING: killing 4226 states (over memory cap)
KLEE: WARNING: killing 4260 states (over memory cap)
KLEE: WARNING: killing 4126 states (over memory cap)
KLEE: WARNING: killing 4121 states (over memory cap)
KLEE: WARNING: killing 6001 states (over memory cap)
KLEE: WARNING: killing 4519 states (over memory cap)
KLEE: WARNING: killing 4346 states (over memory cap)
KLEE: WARNING: killing 4221 states (over memory cap)
KLEE: WARNING: killing 4175 states (over memory cap)
KLEE: WARNING: killing 4251 states (over memory cap)
