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--lustre--libcfs--libcfs.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.: 1136 805 6579 46533
Removed infinite loop in arch_local_irq_restore
Removed infinite loop in arch_local_save_flags
Removed infinite loop in arch_local_irq_disable
Removed infinite loop in sg_assign_page
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 1.6286740303
Removed calls to 'ldv__builtin_va_start' (function is undefined)
Removed calls to 'ldv__builtin_va_end' (function is undefined)
Removed calls to 'panic' (function is undefined)
Removed calls to 'dump_stack' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Defining function call_usermodehelper as symbolic
Removed calls to 'add_wait_queue' (function is undefined)
Removed calls to 'remove_wait_queue' (function is undefined)
Defining function snprintf as symbolic
Removed calls to '__wake_up' (function is undefined)
Defining function kthread_create_on_node as symbolic
Defining function wake_up_process as symbolic
Defining function printk as symbolic
Defining function get_seconds as symbolic
Removed calls to 'down_write' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to 'up_write' (function is undefined)
Defining function filp_open as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function vfs_write as symbolic
Removed calls to '__free_pages' (function is undefined)
Defining function vfs_fsync as symbolic
Defining function filp_close as symbolic
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to '_raw_spin_unlock_bh' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Removed calls to '_raw_spin_lock_bh' (function is undefined)
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function find_next_bit as symbolic
Defining function _raw_spin_lock_irqsave as symbolic
Removed calls to 'do_gettimeofday' (function is undefined)
Defining function __bitmap_weight as symbolic
Defining function default_wake_function as symbolic
Defining function vsnprintf as symbolic
Defining function __printk_ratelimit as symbolic
Defining function alloc_pages_current as symbolic
Defining function mod_timer as symbolic
Defining function del_timer as symbolic
Removed calls to 'recalc_sigpending' (function is undefined)
Removed calls to 'vfree' (function is undefined)
Defining function vmalloc as symbolic
Defining function cpumask_next_and as symbolic
Defining function __cpu_to_node as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function cpumask_of_node as symbolic
Defining function find_first_bit as symbolic
Removed calls to 'trace_hardirqs_off' (function is undefined)
Removed calls to 'lock_acquire' (function is undefined)
Removed calls to 'lock_release' (function is undefined)
Removed calls to 'trace_hardirqs_on' (function is undefined)
Defining function set_cpus_allowed_ptr as symbolic
Defining function prepare_creds as symbolic
Defining function commit_creds as symbolic
Defining function debug_lockdep_rcu_enabled as symbolic
Removed calls to 'sg_init_one' (function is undefined)
Defining function crypto_alloc_base as symbolic
Removed calls to 'sg_init_table' (function is undefined)
Defining function __vmalloc as symbolic
Defining function vmalloc_node as symbolic
Defining function __kmalloc_node as symbolic
Defining function schedule_timeout as symbolic
Defining function sscanf as symbolic
Defining function simple_strtoul as symbolic
Removed calls to 'module_put' (function is undefined)
Removed calls to '__symbol_put' (function is undefined)
Removed calls to 'down_read' (function is undefined)
Removed calls to 'up_read' (function is undefined)
Defining function __symbol_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
Removed calls to '__copy_from_user_overflow' (function is undefined)
Defining function _copy_from_user as symbolic
Defining function try_module_get as symbolic
Defining function strnlen as symbolic
Removed calls to '__rwlock_init' (function is undefined)
Removed calls to '___might_sleep' (function is undefined)
Defining function _cond_resched as symbolic
Defining function seq_printf as symbolic
Removed calls to 'fput' (function is undefined)
Removed calls to 'get_random_bytes' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'abort_exclusive_wait' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Defining function prepare_to_wait_event as symbolic
Defining function capable as symbolic
Defining function proc_dointvec as symbolic
Defining function proc_dostring as symbolic
Defining function proc_dointvec_minmax as symbolic
Defining function proc_doulongvec_minmax as symbolic
Removed calls to 'wait_for_completion' (function is undefined)
Removed calls to 'complete' (function is undefined)
Defining function strncasecmp as symbolic
Removed calls to '_raw_read_lock' (function is undefined)
Removed calls to '_raw_write_lock' (function is undefined)
Removed calls to '_raw_read_unlock' (function is undefined)
Removed calls to '_raw_write_unlock' (function is undefined)
Defining function mutex_trylock as symbolic
Defining function atomic_notifier_chain_register as symbolic
Defining function atomic_notifier_chain_unregister as symbolic
Removed calls to 'unregister_cpu_notifier' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Defining function register_cpu_notifier as symbolic
Defining function __bitmap_and as symbolic
Defining function __request_module as symbolic
Defining function jiffies_to_msecs as symbolic
Defining function crypto_register_shash as symbolic
Defining function crypto_unregister_shash as symbolic
Defining function ldv_setup_4 as symbolic
Defining function ldv_release_4 as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'unregister_sysctl_table' (function is undefined)
Defining function misc_deregister as symbolic
Defining function register_sysctl_table as symbolic
Defining function misc_register as symbolic
Linked our definitions to these undefined functions:
  memchr
  strchr
  strcmp
  strcpy
  strlen
  strncmp
  strncpy
  strrchr
  __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: 1.87460112572
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 1228 639 4074 33557
INFO: Starting verification
WARNING: this target does not support the llvm.returnaddress intrinsic.
KLEE: WARNING ONCE: function "lbug_with_loc" has inline asm
KLEE: WARNING ONCE: function "libcfs_debug_dumplog" has inline asm
KLEE: WARNING ONCE: function "libcfs_debug_dumplog_internal" has inline asm
KLEE: WARNING ONCE: function "cfs_tracefile_dump_all_pages" has inline asm
KLEE: WARNING ONCE: function "cfs_trace_assertion_failed" has inline asm
KLEE: WARNING ONCE: function "cfs_tage_free" has inline asm
KLEE: WARNING ONCE: function "cfs_set_ptldebug_header" has inline asm
KLEE: WARNING ONCE: function "libcfs_debug_vmsg2" has inline asm
KLEE: WARNING ONCE: function "cfs_tage_alloc" has inline asm
KLEE: WARNING ONCE: function "cfs_block_allsigs" has inline asm
KLEE: WARNING ONCE: function "cfs_block_sigs" has inline asm
KLEE: WARNING ONCE: function "cfs_block_sigsinv" has inline asm
KLEE: WARNING ONCE: function "cfs_restore_sigs" has inline asm
KLEE: WARNING ONCE: function "cfs_signal_pending" has inline asm
KLEE: WARNING ONCE: function "cfs_clear_sigpending" has inline asm
KLEE: WARNING ONCE: function "cfs_cpt_table_free" has inline asm
KLEE: WARNING ONCE: function "cfs_cpt_table_alloc" has inline asm
KLEE: WARNING ONCE: function "cfs_cpt_set_cpu" has inline asm
KLEE: WARNING ONCE: function "cfs_cpt_unset_cpu" has inline asm
KLEE: WARNING ONCE: function "cfs_cpt_current" has inline asm
KLEE: WARNING ONCE: function "cfs_cpt_bind" has inline asm
KLEE: WARNING ONCE: function "arch_local_irq_restore" has inline asm
KLEE: WARNING ONCE: function "cfs_cap_raised" has inline asm
KLEE: WARNING ONCE: function "cfs_curproc_cap_pack" has inline asm
KLEE: WARNING ONCE: function "cfs_crypto_hash_update_page" has inline asm
KLEE: WARNING ONCE: function "__cfs_fail_check_set" has inline asm
KLEE: WARNING ONCE: function "__cfs_fail_timeout_set" has inline asm
KLEE: WARNING ONCE: function "cfs_free_nidlist" has inline asm
KLEE: WARNING ONCE: function "cfs_expr_list_free" has inline asm
KLEE: WARNING ONCE: function "cfs_parse_nidlist" has inline asm
KLEE: WARNING ONCE: function "libcfs_psdev_open___0" has inline asm
KLEE: WARNING ONCE: function "libcfs_psdev_release___0" has inline asm
KLEE: WARNING ONCE: function "libcfs_ioctl___0" has inline asm
KLEE: WARNING ONCE: function "cfs_expr_list_values" has inline asm
KLEE: WARNING ONCE: function "cfs_expr_list_parse" has inline asm
KLEE: WARNING ONCE: function "cfs_range_expr_parse" has inline asm
KLEE: WARNING ONCE: function "cfs_hash_bd_add_locked" has inline asm
KLEE: WARNING ONCE: function "cfs_hash_bd_del_locked" has inline asm
KLEE: WARNING ONCE: function "cfs_hash_create" has inline asm
KLEE: WARNING ONCE: function "cfs_hash_buckets_realloc" has inline asm
KLEE: WARNING ONCE: function "cfs_hash_buckets_free" has inline asm
KLEE: WARNING ONCE: function "cfs_wi_exit" has inline asm
KLEE: WARNING ONCE: function "cfs_hash_getref" has inline asm
KLEE: WARNING ONCE: function "cfs_hash_putref" has inline asm
KLEE: WARNING ONCE: function "cfs_wi_deschedule" has inline asm
KLEE: WARNING ONCE: function "cfs_wi_schedule" has inline asm
KLEE: WARNING ONCE: function "cfs_hash_debug_str" has inline asm
KLEE: WARNING ONCE: function "libcfs_kkuc_msg_put" has inline asm
KLEE: WARNING ONCE: function "cfs_wi_sched_destroy" has inline asm
KLEE: WARNING ONCE: function "cfs_wi_sched_create" has inline asm
KLEE: WARNING ONCE: function "cfs_percpt_free" has inline asm
KLEE: WARNING ONCE: function "cfs_percpt_alloc" has inline asm
KLEE: WARNING ONCE: function "cfs_percpt_current" has inline asm
KLEE: WARNING ONCE: function "cfs_array_free" has inline asm
KLEE: WARNING ONCE: function "cfs_array_alloc" has inline asm
KLEE: WARNING ONCE: function "cfs_percpt_lock_free" has inline asm
KLEE: WARNING ONCE: function "cfs_percpt_lock_alloc" has inline asm
KLEE: WARNING ONCE: function "cfs_percpt_lock" has inline asm
KLEE: WARNING ONCE: function "panic_notifier" has inline asm
KLEE: WARNING ONCE: function "cfs_cpu_notify" has inline asm
KLEE: WARNING ONCE: function "tracefiled" has inline asm
KLEE: WARNING ONCE: function "__proc_cpt_table" has inline asm
KLEE: WARNING ONCE: function "cfs_trace_buf_idx_get" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_7" has inline asm
KLEE: WARNING ONCE: function "cfs_cpu_fini" has inline asm
KLEE: WARNING ONCE: function "cfs_cpu_init" has inline asm
KLEE: WARNING ONCE: function "cfs_wi_shutdown" 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_f996f0cb-33b7-4571-944d-0d20596f7d20/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8UHqMS/linux-4.2-rc1.tar.xz-32_7a-drivers--staging--lustre--lustre--libcfs--libcfs.ko-entry_point_true-unreach-call.cil.out.c:16701: divide by zero
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: ERROR: concretized symbolic size to 2^17,analysis may be unsound
KLEE: WARNING ONCE: Large alloc: 3233857728 bytes.  KLEE may run out of memory.
KLEE: output directory is "/tmp/symbiotic-8UHqMS/klee-out-0"
KLEE: Using STP solver backend
WARNING: this target does not support the llvm.returnaddress intrinsic.
KLEE: WARNING ONCE: function "lbug_with_loc" has inline asm
KLEE: WARNING ONCE: function "libcfs_debug_dumplog" has inline asm
KLEE: WARNING ONCE: function "libcfs_debug_dumplog_internal" has inline asm
KLEE: WARNING ONCE: function "cfs_tracefile_dump_all_pages" has inline asm
KLEE: WARNING ONCE: function "cfs_trace_assertion_failed" has inline asm
KLEE: WARNING ONCE: function "cfs_tage_free" has inline asm
KLEE: WARNING ONCE: function "cfs_set_ptldebug_header" has inline asm
KLEE: WARNING ONCE: function "libcfs_debug_vmsg2" has inline asm
KLEE: WARNING ONCE: function "cfs_tage_alloc" has inline asm
KLEE: WARNING ONCE: function "cfs_block_allsigs" has inline asm
KLEE: WARNING ONCE: function "cfs_block_sigs" has inline asm
KLEE: WARNING ONCE: function "cfs_block_sigsinv" has inline asm
KLEE: WARNING ONCE: function "cfs_restore_sigs" has inline asm
KLEE: WARNING ONCE: function "cfs_signal_pending" has inline asm
KLEE: WARNING ONCE: function "cfs_clear_sigpending" has inline asm
KLEE: WARNING ONCE: function "cfs_cpt_table_free" has inline asm
KLEE: WARNING ONCE: function "cfs_cpt_table_alloc" has inline asm
KLEE: WARNING ONCE: function "cfs_cpt_set_cpu" has inline asm
KLEE: WARNING ONCE: function "cfs_cpt_unset_cpu" has inline asm
KLEE: WARNING ONCE: function "cfs_cpt_current" has inline asm
KLEE: WARNING ONCE: function "cfs_cpt_bind" has inline asm
KLEE: WARNING ONCE: function "arch_local_irq_restore" has inline asm
KLEE: WARNING ONCE: function "cfs_cap_raised" has inline asm
KLEE: WARNING ONCE: function "cfs_curproc_cap_pack" has inline asm
KLEE: WARNING ONCE: function "cfs_crypto_hash_update_page" has inline asm
KLEE: WARNING ONCE: function "__cfs_fail_check_set" has inline asm
KLEE: WARNING ONCE: function "__cfs_fail_timeout_set" has inline asm
KLEE: WARNING ONCE: function "cfs_free_nidlist" has inline asm
KLEE: WARNING ONCE: function "cfs_expr_list_free" has inline asm
KLEE: WARNING ONCE: function "cfs_parse_nidlist" has inline asm
KLEE: WARNING ONCE: function "libcfs_psdev_open___0" has inline asm
KLEE: WARNING ONCE: function "libcfs_psdev_release___0" has inline asm
KLEE: WARNING ONCE: function "libcfs_ioctl___0" has inline asm
KLEE: WARNING ONCE: function "cfs_expr_list_values" has inline asm
KLEE: WARNING ONCE: function "cfs_expr_list_parse" has inline asm
KLEE: WARNING ONCE: function "cfs_range_expr_parse" has inline asm
KLEE: WARNING ONCE: function "cfs_hash_bd_add_locked" has inline asm
KLEE: WARNING ONCE: function "cfs_hash_bd_del_locked" has inline asm
KLEE: WARNING ONCE: function "cfs_hash_create" has inline asm
KLEE: WARNING ONCE: function "cfs_hash_buckets_realloc" has inline asm
KLEE: WARNING ONCE: function "cfs_hash_buckets_free" has inline asm
KLEE: WARNING ONCE: function "cfs_wi_exit" has inline asm
KLEE: WARNING ONCE: function "cfs_hash_getref" has inline asm
KLEE: WARNING ONCE: function "cfs_hash_putref" has inline asm
KLEE: WARNING ONCE: function "cfs_wi_deschedule" has inline asm
KLEE: WARNING ONCE: function "cfs_wi_schedule" has inline asm
KLEE: WARNING ONCE: function "cfs_hash_debug_str" has inline asm
KLEE: WARNING ONCE: function "libcfs_kkuc_msg_put" has inline asm
KLEE: WARNING ONCE: function "cfs_wi_sched_destroy" has inline asm
KLEE: WARNING ONCE: function "cfs_wi_sched_create" has inline asm
KLEE: WARNING ONCE: function "cfs_percpt_free" has inline asm
KLEE: WARNING ONCE: function "cfs_percpt_alloc" has inline asm
KLEE: WARNING ONCE: function "cfs_percpt_current" has inline asm
KLEE: WARNING ONCE: function "cfs_array_free" has inline asm
KLEE: WARNING ONCE: function "cfs_array_alloc" has inline asm
KLEE: WARNING ONCE: function "cfs_percpt_lock_free" has inline asm
KLEE: WARNING ONCE: function "cfs_percpt_lock_alloc" has inline asm
KLEE: WARNING ONCE: function "cfs_percpt_lock" has inline asm
KLEE: WARNING ONCE: function "panic_notifier" has inline asm
KLEE: WARNING ONCE: function "cfs_cpu_notify" has inline asm
KLEE: WARNING ONCE: function "tracefiled" has inline asm
KLEE: WARNING ONCE: function "__proc_cpt_table" has inline asm
KLEE: WARNING ONCE: function "cfs_trace_buf_idx_get" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_7" has inline asm
KLEE: WARNING ONCE: function "cfs_cpu_fini" has inline asm
KLEE: WARNING ONCE: function "cfs_cpu_init" has inline asm
KLEE: WARNING ONCE: function "cfs_wi_shutdown" 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_f996f0cb-33b7-4571-944d-0d20596f7d20/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8UHqMS/linux-4.2-rc1.tar.xz-32_7a-drivers--staging--lustre--lustre--libcfs--libcfs.ko-entry_point_true-unreach-call.cil.out.c:16701: divide by zero
KLEE: NOTE: now ignoring this error at this location
KLEE: NOTE: found huge malloc, returning 0
KLEE: WARNING ONCE: ERROR: concretized symbolic size to 2^17,analysis may be unsound
KLEE: WARNING ONCE: Large alloc: 3233857728 bytes.  KLEE may run out of memory.
0  klee            0x00000000012fcca8 llvm::sys::PrintStackTrace(llvm::raw_ostream&) + 56
1  klee            0x00000000012fac7e llvm::sys::RunSignalHandlers() + 62
2  klee            0x00000000012fadcc
3  libpthread.so.0 0x00007fd34722c390
4  klee            0x00000000005d20ab klee::Executor::executeMemoryOperation(klee::ExecutionState&, bool, klee::ref<klee::Expr>, klee::ref<klee::Expr>, klee::KInstruction*) + 75
5  klee            0x00000000005d560d klee::Executor::executeInstruction(klee::ExecutionState&, klee::KInstruction*) + 2285
6  klee            0x00000000005da8c5 klee::Executor::run(klee::ExecutionState&) + 2117
7  klee            0x00000000005daeef klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1391
8  klee            0x0000000000593c63 main + 8867
9  libc.so.6       0x00007fd3465d0830 __libc_start_main + 240
10 klee            0x00000000005bed49 _start + 41
Running the verifier failed
RESULT: unknown
INFO: Total time elapsed: 6.84251904488
