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--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 459 6833 53065
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 1.9132540226
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
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 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 libcfs_deregister_ioctl as symbolic
Defining function strlcpy 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 'ldv_check_final_state' (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
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  strcpy
  strlen
  strncmp
  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.13699507713
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 837 367 3967 41177
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_99b7bef8-0a18-4527-a4f6-bc0125dcbcdb/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-KjDK6k/linux-4.2-rc1.tar.xz-43_2a-drivers--staging--lustre--lnet--selftest--lnet_selftest.ko-entry_point_true-unreach-call.cil.out.c:7494: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 6139 states (over memory cap)
KLEE: WARNING: killing 6208 states (over memory cap)
KLEE: WARNING: killing 6289 states (over memory cap)
KLEE: WARNING: killing 6739 states (over memory cap)
KLEE: WARNING: killing 4721 states (over memory cap)
KLEE: WARNING: killing 6508 states (over memory cap)
KLEE: WARNING: killing 4918 states (over memory cap)
KLEE: WARNING: killing 4952 states (over memory cap)
KLEE: WARNING: killing 4895 states (over memory cap)
KLEE: WARNING: killing 4695 states (over memory cap)
KLEE: WARNING: killing 4911 states (over memory cap)
KLEE: WARNING: killing 4849 states (over memory cap)
KLEE: WARNING: killing 4699 states (over memory cap)
KLEE: WARNING: killing 4816 states (over memory cap)
KLEE: WARNING: killing 4800 states (over memory cap)
KLEE: WARNING: killing 4696 states (over memory cap)
KLEE: WARNING: killing 4905 states (over memory cap)
KLEE: WARNING: killing 4712 states (over memory cap)
KLEE: WARNING: killing 4787 states (over memory cap)
KLEE: WARNING: killing 4731 states (over memory cap)
KLEE: WARNING: killing 4808 states (over memory cap)
KLEE: WARNING: killing 4619 states (over memory cap)
KLEE: WARNING: killing 4876 states (over memory cap)
KLEE: WARNING: killing 4467 states (over memory cap)
KLEE: WARNING: killing 4805 states (over memory cap)
KLEE: WARNING: killing 4532 states (over memory cap)
KLEE: WARNING: killing 4699 states (over memory cap)
KLEE: WARNING: killing 4421 states (over memory cap)
KLEE: WARNING: killing 4452 states (over memory cap)
KLEE: WARNING: killing 4663 states (over memory cap)
KLEE: WARNING: killing 4652 states (over memory cap)
KLEE: WARNING: killing 4471 states (over memory cap)
KLEE: WARNING: killing 4721 states (over memory cap)
KLEE: WARNING: killing 4625 states (over memory cap)
KLEE: WARNING: killing 4485 states (over memory cap)
KLEE: WARNING: killing 4607 states (over memory cap)
KLEE: WARNING: killing 4729 states (over memory cap)
KLEE: WARNING: killing 4590 states (over memory cap)
KLEE: WARNING: killing 4412 states (over memory cap)
KLEE: WARNING: killing 4489 states (over memory cap)
KLEE: WARNING: killing 4610 states (over memory cap)
KLEE: WARNING: killing 4642 states (over memory cap)
KLEE: WARNING: killing 4549 states (over memory cap)
KLEE: WARNING: killing 4497 states (over memory cap)
KLEE: WARNING: killing 4405 states (over memory cap)
KLEE: WARNING: killing 4566 states (over memory cap)
KLEE: WARNING: killing 4643 states (over memory cap)
KLEE: WARNING: killing 4466 states (over memory cap)
KLEE: WARNING: killing 4544 states (over memory cap)
KLEE: WARNING: killing 4536 states (over memory cap)
KLEE: WARNING: killing 4446 states (over memory cap)
KLEE: WARNING: killing 4483 states (over memory cap)
KLEE: WARNING: killing 4473 states (over memory cap)
KLEE: WARNING: killing 4339 states (over memory cap)
KLEE: WARNING: killing 4540 states (over memory cap)
klee: /var/xchalup4/symbiotic/klee/include/klee/Internal/ADT/DiscretePDF.inc:116: void klee::DiscretePDF<T>::remove(T) [with T = klee::ExecutionState*]: Assertion `0 && "remove: argument(item) not in tree"' failed.
KLEE: output directory is "/tmp/symbiotic-KjDK6k/klee-out-0"
KLEE: Using STP solver backend
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_99b7bef8-0a18-4527-a4f6-bc0125dcbcdb/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-KjDK6k/linux-4.2-rc1.tar.xz-43_2a-drivers--staging--lustre--lnet--selftest--lnet_selftest.ko-entry_point_true-unreach-call.cil.out.c:7494: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 6139 states (over memory cap)
KLEE: WARNING: killing 6208 states (over memory cap)
KLEE: WARNING: killing 6289 states (over memory cap)
KLEE: WARNING: killing 6739 states (over memory cap)
KLEE: WARNING: killing 4721 states (over memory cap)
KLEE: WARNING: killing 6508 states (over memory cap)
KLEE: WARNING: killing 4918 states (over memory cap)
KLEE: WARNING: killing 4952 states (over memory cap)
KLEE: WARNING: killing 4895 states (over memory cap)
KLEE: WARNING: killing 4695 states (over memory cap)
KLEE: WARNING: killing 4911 states (over memory cap)
KLEE: WARNING: killing 4849 states (over memory cap)
KLEE: WARNING: killing 4699 states (over memory cap)
KLEE: WARNING: killing 4816 states (over memory cap)
KLEE: WARNING: killing 4800 states (over memory cap)
KLEE: WARNING: killing 4696 states (over memory cap)
KLEE: WARNING: killing 4905 states (over memory cap)
KLEE: WARNING: killing 4712 states (over memory cap)
KLEE: WARNING: killing 4787 states (over memory cap)
KLEE: WARNING: killing 4731 states (over memory cap)
KLEE: WARNING: killing 4808 states (over memory cap)
KLEE: WARNING: killing 4619 states (over memory cap)
KLEE: WARNING: killing 4876 states (over memory cap)
KLEE: WARNING: killing 4467 states (over memory cap)
KLEE: WARNING: killing 4805 states (over memory cap)
KLEE: WARNING: killing 4532 states (over memory cap)
KLEE: WARNING: killing 4699 states (over memory cap)
KLEE: WARNING: killing 4421 states (over memory cap)
KLEE: WARNING: killing 4452 states (over memory cap)
KLEE: WARNING: killing 4663 states (over memory cap)
KLEE: WARNING: killing 4652 states (over memory cap)
KLEE: WARNING: killing 4471 states (over memory cap)
KLEE: WARNING: killing 4721 states (over memory cap)
KLEE: WARNING: killing 4625 states (over memory cap)
KLEE: WARNING: killing 4485 states (over memory cap)
KLEE: WARNING: killing 4607 states (over memory cap)
KLEE: WARNING: killing 4729 states (over memory cap)
KLEE: WARNING: killing 4590 states (over memory cap)
KLEE: WARNING: killing 4412 states (over memory cap)
KLEE: WARNING: killing 4489 states (over memory cap)
KLEE: WARNING: killing 4610 states (over memory cap)
KLEE: WARNING: killing 4642 states (over memory cap)
KLEE: WARNING: killing 4549 states (over memory cap)
KLEE: WARNING: killing 4497 states (over memory cap)
KLEE: WARNING: killing 4405 states (over memory cap)
KLEE: WARNING: killing 4566 states (over memory cap)
KLEE: WARNING: killing 4643 states (over memory cap)
KLEE: WARNING: killing 4466 states (over memory cap)
KLEE: WARNING: killing 4544 states (over memory cap)
KLEE: WARNING: killing 4536 states (over memory cap)
KLEE: WARNING: killing 4446 states (over memory cap)
KLEE: WARNING: killing 4483 states (over memory cap)
KLEE: WARNING: killing 4473 states (over memory cap)
KLEE: WARNING: killing 4339 states (over memory cap)
KLEE: WARNING: killing 4540 states (over memory cap)
klee: /var/xchalup4/symbiotic/klee/include/klee/Internal/ADT/DiscretePDF.inc:116: void klee::DiscretePDF<T>::remove(T) [with T = klee::ExecutionState*]: Assertion `0 && "remove: argument(item) not in tree"' failed.
0  klee            0x00000000012fcca8 llvm::sys::PrintStackTrace(llvm::raw_ostream&) + 56
1  klee            0x00000000012fac7e llvm::sys::RunSignalHandlers() + 62
2  klee            0x00000000012fadcc
3  libpthread.so.0 0x00007f9cf020c390
4  libc.so.6       0x00007f9cef5c5428 gsignal + 56
5  libc.so.6       0x00007f9cef5c702a abort + 362
6  libc.so.6       0x00007f9cef5bdbd7
7  libc.so.6       0x00007f9cef5bdc82
8  klee            0x000000000061be59 klee::DiscretePDF<klee::ExecutionState*>::remove(klee::ExecutionState*) + 73
9  klee            0x00000000006195f1 klee::WeightedRandomSearcher::update(klee::ExecutionState*, std::vector<klee::ExecutionState*, std::allocator<klee::ExecutionState*> > const&, std::vector<klee::ExecutionState*, std::allocator<klee::ExecutionState*> > const&) + 241
10 klee            0x0000000000617416 klee::InterleavedSearcher::update(klee::ExecutionState*, std::vector<klee::ExecutionState*, std::allocator<klee::ExecutionState*> > const&, std::vector<klee::ExecutionState*, std::allocator<klee::ExecutionState*> > const&) + 54
11 klee            0x00000000005cecfe klee::Executor::updateStates(klee::ExecutionState*) + 46
12 klee            0x00000000005da8eb klee::Executor::run(klee::ExecutionState&) + 2155
13 klee            0x00000000005daeef klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1391
14 klee            0x0000000000593c63 main + 8867
15 libc.so.6       0x00007f9cef5b0830 __libc_start_main + 240
16 klee            0x00000000005bed49 _start + 41
Running the verifier failed
RESULT: unknown
INFO: Total time elapsed: 490.384895086
