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-08_1a-drivers--staging--lustre--lnet--selftest--lnet_selftest.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.: 714 336 6716 51141
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 1.91339802742
Removed calls to 'lbug_with_loc' (function is undefined)
Removed calls to 'vfree' (function is undefined)
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function libcfs_debug_msg as symbolic
Defining function vmalloc as symbolic
Removed calls to '__might_fault' (function is undefined)
Removed calls to '__copy_from_user_overflow' (function is undefined)
Defining function get_seconds as symbolic
Removed calls to '__copy_to_user_overflow' (function is undefined)
Defining function _copy_to_user as symbolic
Removed calls to '__list_add' (function is undefined)
Defining function libcfs_id2str as symbolic
Removed calls to 'list_del' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to '__free_pages' (function is undefined)
Defining function prepare_to_wait_event as symbolic
Defining function schedule_timeout as symbolic
Defining function libcfs_nid2str as symbolic
Removed calls to 'cfs_wi_schedule' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Defining function lnet_cpt_of_nid as symbolic
Removed calls to 'schedule' (function is undefined)
Removed calls to 'cfs_wi_exit' (function is undefined)
Defining function LNetMDUnlink as symbolic
Defining function LNetMDBind as symbolic
Defining function LNetPut as symbolic
Defining function LNetGet as symbolic
Defining function LNetMEAttach as symbolic
Defining function LNetMDAttach as symbolic
Defining function LNetMEUnlink as symbolic
Defining function alloc_pages_current as symbolic
Defining function LNetGetId as symbolic
Defining function _copy_from_user as symbolic
Removed calls to '__mutex_init' (function is undefined)
Defining function libcfs_register_ioctl as symbolic
Defining function cfs_percpt_number as symbolic
Removed calls to 'cfs_percpt_free' (function is undefined)
Defining function cfs_wi_deschedule as symbolic
Defining function cfs_percpt_alloc as symbolic
Defining function cfs_cpt_number as symbolic
Defining function cfs_cpt_spread_node as symbolic
Defining function __kmalloc_node as symbolic
Defining function libcfs_deregister_ioctl as symbolic
Defining function strlcpy as symbolic
Defining function vmalloc_node as symbolic
Defining function __alloc_pages_nodemask as symbolic
Removed calls to 'lnet_counters_get' (function is undefined)
Defining function current_kernel_time as symbolic
Defining function kthread_create_on_node as symbolic
Defining function wake_up_process as symbolic
Defining function cfs_block_allsigs as symbolic
Defining function LNetNIInit as symbolic
Defining function LNetEQAlloc as symbolic
Defining function LNetSetLazyPortal as symbolic
Defining function LNetClearLazyPortal as symbolic
Defining function LNetEQFree as symbolic
Defining function LNetNIFini as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'cfs_wi_sched_destroy' (function is undefined)
Defining function cfs_wi_sched_create as symbolic
Defining function cfs_cpt_weight as symbolic
Linked our definitions to these undefined functions:
  strcpy
  strlen
  strncmp
  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.18471193314
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 837 248 3608 39197
INFO: Starting verification
KLEE: WARNING ONCE: function "lstcon_ioctl_entry" has inline asm
KLEE: WARNING ONCE: function "lstcon_session_info" has inline asm
KLEE: WARNING ONCE: function "lstcon_group_info" has inline asm
KLEE: WARNING ONCE: function "lstcon_batch_add" has inline asm
KLEE: WARNING ONCE: function "lstcon_batch_info" has inline asm
KLEE: WARNING ONCE: function "lstcon_test_add" has inline asm
KLEE: WARNING ONCE: function "lstcon_group_alloc" has inline asm
KLEE: WARNING ONCE: function "lstcon_group_put" has inline asm
KLEE: WARNING ONCE: function "lstcon_rpc_trans_destroy" has inline asm
KLEE: WARNING ONCE: function "lstcon_rpc_put" has inline asm
KLEE: WARNING ONCE: function "lstcon_rpc_post" has inline asm
KLEE: WARNING ONCE: function "lstcon_rpc_trans_prep" has inline asm
KLEE: WARNING ONCE: function "lstcon_rpc_prep" has inline asm
KLEE: WARNING ONCE: function "lstcon_rpc_init" has inline asm
KLEE: WARNING ONCE: function "lstcon_rpc_done" has inline asm
KLEE: WARNING ONCE: function "srpc_create_client_rpc" has inline asm
KLEE: WARNING ONCE: function "lstcon_ndlink_release" has inline asm
KLEE: WARNING ONCE: function "lstcon_node_put" has inline asm
KLEE: WARNING ONCE: function "lstcon_ndlink_find" has inline asm
KLEE: WARNING ONCE: function "lstcon_rpc_cleanup_wait" has inline asm
KLEE: WARNING ONCE: function "lstcon_batch_destroy" has inline asm
KLEE: WARNING ONCE: function "lstcon_console_init" has inline asm
KLEE: WARNING ONCE: function "srpc_add_service" has inline asm
KLEE: WARNING ONCE: function "srpc_service_add_buffers" has inline asm
KLEE: WARNING ONCE: function "srpc_wait_service_shutdown" has inline asm
KLEE: WARNING ONCE: function "srpc_service_fini" has inline asm
KLEE: WARNING ONCE: function "srpc_add_buffer" has inline asm
KLEE: WARNING ONCE: function "srpc_service_post_buffer" has inline asm
KLEE: WARNING ONCE: function "lstcon_console_fini" has inline asm
KLEE: WARNING ONCE: function "sfw_make_session" has inline asm
KLEE: WARNING ONCE: function "sfw_deactivate_session" has inline asm
KLEE: WARNING ONCE: function "sfw_destroy_session" has inline asm
KLEE: WARNING ONCE: function "sfw_destroy_test_instance" has inline asm
KLEE: WARNING ONCE: function "sfw_test_rpc_done" has inline asm
KLEE: WARNING ONCE: function "sfw_test_unit_done" has inline asm
KLEE: WARNING ONCE: function "srpc_free_bulk" has inline asm
KLEE: WARNING ONCE: function "srpc_alloc_bulk" has inline asm
KLEE: WARNING ONCE: function "brw_client_done_rpc" has inline asm
KLEE: WARNING ONCE: function "sfw_register_test" has inline asm
KLEE: WARNING ONCE: function "ping_client_done_rpc" has inline asm
KLEE: WARNING ONCE: function "sfw_handle_server_rpc" has inline asm
KLEE: WARNING ONCE: function "sfw_shutdown" has inline asm
KLEE: WARNING ONCE: function "srpc_wait_service_shutdown___0" has inline asm
KLEE: WARNING ONCE: function "sfw_add_test" has inline asm
KLEE: WARNING ONCE: function "stt_shutdown" has inline asm
KLEE: WARNING ONCE: function "srpc_server_rpc_done" has inline asm
KLEE: WARNING ONCE: function "srpc_startup" has inline asm
KLEE: WARNING ONCE: function "srpc_lnet_ev_handler" has inline asm
KLEE: WARNING ONCE: function "main" has inline asm
KLEE: WARNING ONCE: function "lnet_selftest_fini" has inline asm
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_70ff75d2-1ca9-4dfb-a2a3-b7637db2ca5e/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-fxMgcM/linux-4.2-rc1.tar.xz-08_1a-drivers--staging--lustre--lnet--selftest--lnet_selftest.ko-entry_point_true-unreach-call.cil.out.c:7384: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 6350 states (over memory cap)
KLEE: WARNING: killing 6045 states (over memory cap)
KLEE: WARNING: killing 6358 states (over memory cap)
KLEE: WARNING: killing 4768 states (over memory cap)
KLEE: WARNING: killing 6743 states (over memory cap)
KLEE: WARNING: killing 4835 states (over memory cap)
KLEE: WARNING: killing 6615 states (over memory cap)
KLEE: WARNING: killing 4666 states (over memory cap)
KLEE: WARNING: killing 4741 states (over memory cap)
KLEE: WARNING: killing 4636 states (over memory cap)
KLEE: WARNING: killing 4897 states (over memory cap)
KLEE: WARNING: killing 4795 states (over memory cap)
KLEE: WARNING: killing 5010 states (over memory cap)
KLEE: WARNING: killing 4809 states (over memory cap)
KLEE: WARNING: killing 4842 states (over memory cap)
KLEE: WARNING: killing 5052 states (over memory cap)
KLEE: WARNING: killing 5040 states (over memory cap)
KLEE: WARNING: killing 4801 states (over memory cap)
KLEE: WARNING: killing 4699 states (over memory cap)
KLEE: WARNING: killing 4680 states (over memory cap)
KLEE: WARNING: killing 4625 states (over memory cap)
KLEE: WARNING: killing 4656 states (over memory cap)
KLEE: WARNING: killing 4467 states (over memory cap)
KLEE: WARNING: killing 4630 states (over memory cap)
KLEE: WARNING: killing 4486 states (over memory cap)
KLEE: WARNING: killing 4959 states (over memory cap)
KLEE: WARNING: killing 4683 states (over memory cap)
KLEE: WARNING: killing 4807 states (over memory cap)
KLEE: WARNING: killing 4666 states (over memory cap)
KLEE: WARNING: killing 4741 states (over memory cap)
KLEE: WARNING: killing 4513 states (over memory cap)
KLEE: WARNING: killing 4763 states (over memory cap)
KLEE: WARNING: killing 4709 states (over memory cap)
KLEE: WARNING: killing 4353 states (over memory cap)
KLEE: WARNING: killing 4340 states (over memory cap)
KLEE: WARNING: killing 4717 states (over memory cap)
KLEE: WARNING: killing 4537 states (over memory cap)
KLEE: WARNING: killing 4530 states (over memory cap)
KLEE: WARNING: killing 4734 states (over memory cap)
KLEE: WARNING: killing 4383 states (over memory cap)
KLEE: WARNING: killing 4460 states (over memory cap)
KLEE: WARNING: killing 4663 states (over memory cap)
KLEE: WARNING: killing 4743 states (over memory cap)
KLEE: WARNING: killing 4393 states (over memory cap)
KLEE: WARNING: killing 4428 states (over memory cap)
KLEE: WARNING: killing 4587 states (over memory cap)
KLEE: WARNING: killing 4458 states (over memory cap)
KLEE: WARNING: killing 4578 states (over memory cap)
KLEE: WARNING: killing 4360 states (over memory cap)
KLEE: WARNING: killing 4563 states (over memory cap)
KLEE: WARNING: killing 4431 states (over memory cap)
KLEE: WARNING: killing 4507 states (over memory cap)
KLEE: WARNING: killing 4584 states (over memory cap)
KLEE: WARNING: killing 4658 states (over memory cap)
KLEE: WARNING: killing 4482 states (over memory cap)
KLEE: WARNING: killing 4476 states (over memory cap)
KLEE: WARNING: killing 4467 states (over memory cap)
KLEE: WARNING: killing 4545 states (over memory cap)
KLEE: WARNING: killing 4492 states (over memory cap)
KLEE: WARNING: killing 4400 states (over memory cap)
KLEE: WARNING: killing 4563 states (over memory cap)
KLEE: WARNING: killing 4472 states (over memory cap)
KLEE: WARNING: killing 4545 states (over memory cap)
KLEE: WARNING: killing 4460 states (over memory cap)
KLEE: WARNING: killing 4616 states (over memory cap)
KLEE: WARNING: killing 4486 states (over memory cap)
KLEE: WARNING: killing 4397 states (over memory cap)
KLEE: WARNING: killing 4471 states (over memory cap)
KLEE: WARNING: killing 4544 states (over memory cap)
KLEE: WARNING: killing 4457 states (over memory cap)
KLEE: WARNING: killing 4611 states (over memory cap)
KLEE: WARNING: killing 4605 states (over memory cap)
KLEE: WARNING: killing 4517 states (over memory cap)
KLEE: WARNING: killing 4591 states (over memory cap)
KLEE: WARNING: killing 4502 states (over memory cap)
KLEE: WARNING: killing 4495 states (over memory cap)
KLEE: WARNING: killing 4529 states (over memory cap)
KLEE: WARNING: killing 4485 states (over memory cap)
KLEE: WARNING: killing 4396 states (over memory cap)
KLEE: WARNING: killing 4506 states (over memory cap)
KLEE: WARNING: killing 4619 states (over memory cap)
KLEE: WARNING: killing 4571 states (over memory cap)
KLEE: WARNING: killing 4446 states (over memory cap)
KLEE: WARNING: killing 4558 states (over memory cap)
KLEE: WARNING: killing 4593 states (over memory cap)
KLEE: WARNING: killing 4424 states (over memory cap)
KLEE: WARNING: killing 4339 states (over memory cap)
KLEE: WARNING: killing 4408 states (over memory cap)
KLEE: WARNING: killing 4520 states (over memory cap)
KLEE: WARNING: killing 4435 states (over memory cap)
KLEE: WARNING: killing 4625 states (over memory cap)
KLEE: WARNING: killing 4500 states (over memory cap)
KLEE: WARNING: killing 4416 states (over memory cap)
KLEE: WARNING: killing 4683 states (over memory cap)
KLEE: WARNING: killing 4601 states (over memory cap)
KLEE: WARNING: killing 4439 states (over memory cap)
KLEE: WARNING: killing 4433 states (over memory cap)
KLEE: WARNING: killing 4269 states (over memory cap)
