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--lustre--obdecho--obdecho.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.: 281 212 2025 15121
Removed infinite loop in get_page
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.719824075699
Removed calls to 'lbug_with_loc' (function is undefined)
Removed calls to 'lprocfs_counter_add' (function is undefined)
Removed calls to 'cl_2queue_init' (function is undefined)
Removed calls to 'cl_page_put' (function is undefined)
Removed calls to 'cl_2queue_add' (function is undefined)
Removed calls to 'cl_page_clip' (function is undefined)
Removed calls to 'cl_2queue_discard' (function is undefined)
Removed calls to 'cl_2queue_disown' (function is undefined)
Removed calls to 'cl_2queue_fini' (function is undefined)
Removed calls to 'cl_io_fini' (function is undefined)
Removed calls to 'cl_env_put' (function is undefined)
Removed calls to 'lprocfs_counter_sub' (function is undefined)
Removed calls to '__free_pages' (function is undefined)
Removed calls to 'obdo_to_ioobj' (function is undefined)
Removed calls to 'lu_context_exit' (function is undefined)
Removed calls to 'lu_context_enter' (function is undefined)
Removed calls to 'lu_env_fini' (function is undefined)
Removed calls to 'ldlm_lock_decref' (function is undefined)
Defining function class_disconnect as symbolic
Defining function class_connect as symbolic
Defining function class_conn2export as symbolic
Defining function lu_env_init as symbolic
Defining function capable as symbolic
Defining function libcfs_debug_msg as symbolic
Defining function cl_env_get as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'cl_lock_get' (function is undefined)
Removed calls to 'cl_unuse' (function is undefined)
Removed calls to 'cl_lock_release' (function is undefined)
Removed calls to 'cl_lock_mutex_get' (function is undefined)
Removed calls to 'cl_lock_cancel' (function is undefined)
Removed calls to 'cl_lock_delete' (function is undefined)
Removed calls to 'cl_lock_mutex_put' (function is undefined)
Removed calls to 'cl_lock_put' (function is undefined)
Defining function cl_io_init as symbolic
Removed calls to '__list_add' (function is undefined)
Defining function cl_index as symbolic
Defining function cl_lock_request as symbolic
Defining function cl_wait as symbolic
Defining function cl_lock_at as symbolic
Defining function lu_context_key_get as symbolic
Removed calls to '__might_fault' (function is undefined)
Removed calls to '__copy_to_user_overflow' (function is undefined)
Defining function _copy_to_user as symbolic
Defining function class_exp2obd as symbolic
Removed calls to '__might_sleep' (function is undefined)
Defining function block_debug_check as symbolic
Defining function block_debug_setup as symbolic
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function cl_page_size as symbolic
Defining function cl_page_find as symbolic
Defining function cl_page_own as symbolic
Defining function cl_io_submit_sync as symbolic
Defining function cl_page_cache_add as symbolic
Defining function lprocfs_read_helper as symbolic
Removed calls to 'cl_object_put' (function is undefined)
Defining function cl_object_find as symbolic
Defining function cfs_rand as symbolic
Removed calls to '__copy_from_user_overflow' (function is undefined)
Defining function _copy_from_user as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'cl_site_fini' (function is undefined)
Removed calls to 'lu_device_fini' (function is undefined)
Removed calls to 'ldv__builtin_va_start' (function is undefined)
Removed calls to 'ldv__builtin_va_arg' (function is undefined)
Removed calls to 'ldv__builtin_va_end' (function is undefined)
Removed calls to 'lu_context_key_degister_many' (function is undefined)
Removed calls to 'lu_context_key_revive_many' (function is undefined)
Removed calls to 'lu_context_key_quiesce_many' (function is undefined)
Defining function lu_context_key_register_many as symbolic
Defining function lu_site_purge as symbolic
Defining function schedule_timeout as symbolic
Defining function class_name2obd as symbolic
Defining function cl_site_init as symbolic
Defining function lu_site_init_finish as symbolic
Defining function lu_device_init as symbolic
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'cl_page_delete' (function is undefined)
Removed calls to 'put_page' (function is undefined)
Defining function mutex_trylock as symbolic
Removed calls to 'kmem_cache_free' (function is undefined)
Defining function obd_alloc_fail as symbolic
Defining function __cfs_fail_check_set as symbolic
Removed calls to 'lu_object_add_top' (function is undefined)
Defining function cl_object_header_init as symbolic
Defining function lu_object_init as symbolic
Removed calls to 'dump_page' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'cl_page_slice_add' (function is undefined)
Removed calls to 'cl_lock_slice_add' (function is undefined)
Defining function __get_page_tail as symbolic
Removed calls to 'lu_object_add' (function is undefined)
Removed calls to 'lu_object_fini' (function is undefined)
Removed calls to 'lu_object_header_fini' (function is undefined)
Removed calls to 'lu_kmem_fini' (function is undefined)
Defining function lu_kmem_init as symbolic
Defining function class_register_type as symbolic
Defining function class_unregister_type as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'ldv_check_final_state' (function is undefined)
Defining function ldv_probe_1 as symbolic
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  strcmp
  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: 0.816136837006
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 418 163 1110 10705
INFO: Starting verification
KLEE: WARNING ONCE: function "cl_echo_enqueue0" has inline asm
KLEE: WARNING ONCE: function "cl_echo_cancel0" has inline asm
KLEE: WARNING ONCE: function "cl_echo_object_put" has inline asm
KLEE: WARNING ONCE: function "echo_device_free" has inline asm
KLEE: WARNING ONCE: function "echo_page_fini" has inline asm
KLEE: WARNING ONCE: function "echo_thread_key_init" has inline asm
KLEE: WARNING ONCE: function "echo_session_key_init" has inline asm
KLEE: WARNING ONCE: function "echo_object_alloc" has inline asm
KLEE: WARNING ONCE: function "echo_page_init" has inline asm
KLEE: WARNING ONCE: function "echo_lock_init" has inline asm
KLEE: WARNING ONCE: function "main" 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_64b61796-bd96-49e4-8f67-b823aa7c6bbe/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 18082 states (over memory cap)
KLEE: WARNING: killing 14745 states (over memory cap)
KLEE: WARNING: killing 13582 states (over memory cap)
KLEE: WARNING: killing 14168 states (over memory cap)
KLEE: WARNING: killing 13681 states (over memory cap)
KLEE: WARNING: killing 13653 states (over memory cap)
KLEE: WARNING: killing 13957 states (over memory cap)
KLEE: WARNING: killing 14041 states (over memory cap)
KLEE: WARNING: killing 14300 states (over memory cap)
KLEE: WARNING: killing 15165 states (over memory cap)
KLEE: WARNING: killing 14917 states (over memory cap)
KLEE: WARNING: killing 15118 states (over memory cap)
KLEE: WARNING: killing 16104 states (over memory cap)
KLEE: WARNING: killing 15639 states (over memory cap)
KLEE: WARNING: killing 15618 states (over memory cap)
KLEE: WARNING: killing 14821 states (over memory cap)
KLEE: WARNING: killing 15693 states (over memory cap)
KLEE: WARNING: killing 15114 states (over memory cap)
KLEE: WARNING: killing 14930 states (over memory cap)
KLEE: WARNING: killing 14966 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-MUl7Ll/linux-4.2-rc1.tar.xz-43_2a-drivers--staging--lustre--lustre--obdecho--obdecho.ko-entry_point_true-unreach-call.cil.out.c:11770: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15493 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-MUl7Ll/linux-4.2-rc1.tar.xz-43_2a-drivers--staging--lustre--lustre--obdecho--obdecho.ko-entry_point_true-unreach-call.cil.out.c:8954: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-MUl7Ll/linux-4.2-rc1.tar.xz-43_2a-drivers--staging--lustre--lustre--obdecho--obdecho.ko-entry_point_true-unreach-call.cil.out.c:8954: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-MUl7Ll/linux-4.2-rc1.tar.xz-43_2a-drivers--staging--lustre--lustre--obdecho--obdecho.ko-entry_point_true-unreach-call.cil.out.c:12702: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15036 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-MUl7Ll/linux-4.2-rc1.tar.xz-43_2a-drivers--staging--lustre--lustre--obdecho--obdecho.ko-entry_point_true-unreach-call.cil.out.c:9008: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-MUl7Ll/linux-4.2-rc1.tar.xz-43_2a-drivers--staging--lustre--lustre--obdecho--obdecho.ko-entry_point_true-unreach-call.cil.out.c:8954: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 14958 states (over memory cap)
KLEE: WARNING: killing 15099 states (over memory cap)
KLEE: WARNING: killing 14694 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-MUl7Ll/linux-4.2-rc1.tar.xz-43_2a-drivers--staging--lustre--lustre--obdecho--obdecho.ko-entry_point_true-unreach-call.cil.out.c:8911: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-MUl7Ll/linux-4.2-rc1.tar.xz-43_2a-drivers--staging--lustre--lustre--obdecho--obdecho.ko-entry_point_true-unreach-call.cil.out.c:13075: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15053 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-MUl7Ll/linux-4.2-rc1.tar.xz-43_2a-drivers--staging--lustre--lustre--obdecho--obdecho.ko-entry_point_true-unreach-call.cil.out.c:9008: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 14489 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-MUl7Ll/linux-4.2-rc1.tar.xz-43_2a-drivers--staging--lustre--lustre--obdecho--obdecho.ko-entry_point_true-unreach-call.cil.out.c:12280: reached "unreachable" instruction
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-MUl7Ll/linux-4.2-rc1.tar.xz-43_2a-drivers--staging--lustre--lustre--obdecho--obdecho.ko-entry_point_true-unreach-call.cil.out.c:8911: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 14905 states (over memory cap)
KLEE: WARNING: killing 15210 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-MUl7Ll/linux-4.2-rc1.tar.xz-43_2a-drivers--staging--lustre--lustre--obdecho--obdecho.ko-entry_point_true-unreach-call.cil.out.c:12208: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15197 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-MUl7Ll/linux-4.2-rc1.tar.xz-43_2a-drivers--staging--lustre--lustre--obdecho--obdecho.ko-entry_point_true-unreach-call.cil.out.c:12055: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 14742 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-MUl7Ll/linux-4.2-rc1.tar.xz-43_2a-drivers--staging--lustre--lustre--obdecho--obdecho.ko-entry_point_true-unreach-call.cil.out.c:9008: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15643 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-MUl7Ll/linux-4.2-rc1.tar.xz-43_2a-drivers--staging--lustre--lustre--obdecho--obdecho.ko-entry_point_true-unreach-call.cil.out.c:12730: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-MUl7Ll/linux-4.2-rc1.tar.xz-43_2a-drivers--staging--lustre--lustre--obdecho--obdecho.ko-entry_point_true-unreach-call.cil.out.c:9274: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15353 states (over memory cap)
KLEE: WARNING: killing 15382 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-MUl7Ll/linux-4.2-rc1.tar.xz-43_2a-drivers--staging--lustre--lustre--obdecho--obdecho.ko-entry_point_true-unreach-call.cil.out.c:9008: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15263 states (over memory cap)
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15569 states (over memory cap)
KLEE: WARNING: killing 15494 states (over memory cap)
KLEE: WARNING: killing 15046 states (over memory cap)
KLEE: WARNING: killing 14109 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-MUl7Ll/linux-4.2-rc1.tar.xz-43_2a-drivers--staging--lustre--lustre--obdecho--obdecho.ko-entry_point_true-unreach-call.cil.out.c:13151: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15596 states (over memory cap)
KLEE: WARNING: killing 15312 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-MUl7Ll/linux-4.2-rc1.tar.xz-43_2a-drivers--staging--lustre--lustre--obdecho--obdecho.ko-entry_point_true-unreach-call.cil.out.c:15309: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15086 states (over memory cap)
KLEE: WARNING: killing 15446 states (over memory cap)
KLEE: WARNING: killing 14569 states (over memory cap)
KLEE: WARNING: killing 14871 states (over memory cap)
KLEE: WARNING: killing 15118 states (over memory cap)
KLEE: WARNING: killing 15687 states (over memory cap)
KLEE: WARNING: killing 14333 states (over memory cap)
KLEE: WARNING: killing 15061 states (over memory cap)
KLEE: WARNING: killing 15794 states (over memory cap)
KLEE: WARNING: killing 15142 states (over memory cap)
KLEE: WARNING: killing 15235 states (over memory cap)
KLEE: WARNING: killing 15485 states (over memory cap)
KLEE: WARNING: killing 14571 states (over memory cap)
KLEE: WARNING: killing 14923 states (over memory cap)
KLEE: WARNING: killing 15384 states (over memory cap)
KLEE: WARNING: killing 15156 states (over memory cap)
KLEE: WARNING: killing 15085 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-MUl7Ll/linux-4.2-rc1.tar.xz-43_2a-drivers--staging--lustre--lustre--obdecho--obdecho.ko-entry_point_true-unreach-call.cil.out.c:12840: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15598 states (over memory cap)
KLEE: WARNING: killing 14893 states (over memory cap)
KLEE: WARNING: killing 14877 states (over memory cap)
KLEE: WARNING: killing 15494 states (over memory cap)
KLEE: WARNING: killing 15320 states (over memory cap)
KLEE: WARNING: killing 15305 states (over memory cap)
KLEE: WARNING: killing 14824 states (over memory cap)
KLEE: WARNING: killing 15227 states (over memory cap)
KLEE: WARNING: killing 14375 states (over memory cap)
KLEE: WARNING: killing 15090 states (over memory cap)
KLEE: WARNING: killing 15076 states (over memory cap)
KLEE: WARNING: killing 14802 states (over memory cap)
KLEE: WARNING: killing 15047 states (over memory cap)
KLEE: WARNING: killing 15296 states (over memory cap)
KLEE: WARNING: killing 14965 states (over memory cap)
KLEE: WARNING: killing 15157 states (over memory cap)
KLEE: WARNING: killing 15352 states (over memory cap)
KLEE: WARNING: killing 14920 states (over memory cap)
KLEE: WARNING: killing 14649 states (over memory cap)
KLEE: WARNING: killing 14996 states (over memory cap)
KLEE: WARNING: killing 15350 states (over memory cap)
KLEE: WARNING: killing 15132 states (over memory cap)
KLEE: WARNING: killing 14700 states (over memory cap)
KLEE: WARNING: killing 15458 states (over memory cap)
KLEE: WARNING: killing 15451 states (over memory cap)
KLEE: WARNING: killing 15385 states (over memory cap)
KLEE: WARNING: killing 15007 states (over memory cap)
KLEE: WARNING: killing 14738 states (over memory cap)
KLEE: WARNING: killing 15187 states (over memory cap)
KLEE: WARNING: killing 14966 states (over memory cap)
KLEE: WARNING: killing 15473 states (over memory cap)
KLEE: WARNING: killing 14692 states (over memory cap)
KLEE: WARNING: killing 14727 states (over memory cap)
KLEE: WARNING: killing 14607 states (over memory cap)
KLEE: WARNING: killing 15004 states (over memory cap)
KLEE: WARNING: killing 15296 states (over memory cap)
KLEE: WARNING: killing 15289 states (over memory cap)
KLEE: WARNING: killing 15889 states (over memory cap)
KLEE: WARNING: killing 14594 states (over memory cap)
KLEE: WARNING: killing 15245 states (over memory cap)
KLEE: WARNING: killing 15075 states (over memory cap)
KLEE: WARNING: killing 15371 states (over memory cap)
KLEE: WARNING: killing 15102 states (over memory cap)
KLEE: WARNING: killing 15196 states (over memory cap)
KLEE: WARNING: killing 15033 states (over memory cap)
KLEE: WARNING: killing 15839 states (over memory cap)
KLEE: WARNING: killing 15215 states (over memory cap)
KLEE: WARNING: killing 15409 states (over memory cap)
KLEE: WARNING: killing 15096 states (over memory cap)
KLEE: WARNING: killing 14417 states (over memory cap)
KLEE: WARNING: killing 15066 states (over memory cap)
KLEE: WARNING: killing 15507 states (over memory cap)
KLEE: WARNING: killing 14784 states (over memory cap)
KLEE: WARNING: killing 15635 states (over memory cap)
KLEE: WARNING: killing 15019 states (over memory cap)
KLEE: WARNING: killing 15109 states (over memory cap)
KLEE: WARNING: killing 14384 states (over memory cap)
KLEE: WARNING: killing 15128 states (over memory cap)
KLEE: WARNING: killing 15116 states (over memory cap)
KLEE: WARNING: killing 15148 states (over memory cap)
KLEE: WARNING: killing 14739 states (over memory cap)
KLEE: WARNING: killing 15074 states (over memory cap)
KLEE: WARNING: killing 15110 states (over memory cap)
KLEE: WARNING: killing 15352 states (over memory cap)
KLEE: WARNING: killing 14993 states (over memory cap)
KLEE: WARNING: killing 14831 states (over memory cap)
KLEE: WARNING: killing 15262 states (over memory cap)
KLEE: WARNING: killing 15349 states (over memory cap)
KLEE: WARNING: killing 15391 states (over memory cap)
KLEE: WARNING: killing 15029 states (over memory cap)
KLEE: WARNING: killing 14815 states (over memory cap)
KLEE: WARNING: killing 15055 states (over memory cap)
KLEE: WARNING: killing 15239 states (over memory cap)
KLEE: WARNING: killing 14678 states (over memory cap)
KLEE: WARNING: killing 15360 states (over memory cap)
KLEE: WARNING: killing 14952 states (over memory cap)
KLEE: WARNING: killing 15779 states (over memory cap)
KLEE: WARNING: killing 15128 states (over memory cap)
KLEE: WARNING: killing 14465 states (over memory cap)
KLEE: WARNING: killing 14950 states (over memory cap)
KLEE: WARNING: killing 14736 states (over memory cap)
KLEE: WARNING: killing 14966 states (over memory cap)
KLEE: WARNING: killing 15447 states (over memory cap)
KLEE: WARNING: killing 15682 states (over memory cap)
KLEE: WARNING: killing 15427 states (over memory cap)
KLEE: WARNING: killing 15225 states (over memory cap)
KLEE: WARNING: killing 15309 states (over memory cap)
KLEE: WARNING: killing 15149 states (over memory cap)
KLEE: WARNING: killing 15138 states (over memory cap)
KLEE: WARNING: killing 14434 states (over memory cap)
KLEE: WARNING: killing 14718 states (over memory cap)
KLEE: WARNING: killing 14752 states (over memory cap)
KLEE: WARNING: killing 15027 states (over memory cap)
KLEE: WARNING: killing 14964 states (over memory cap)
