bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.14/linux-3.14__complex_emg__linux-kernel-locking-spinlock__fs-autofs4-autofs4_true-unreach-call.cil.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.: 257 401 2765 17268
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.791067123413
Removed calls to 'put_pid' (function is undefined)
Removed calls to 'kill_litter_super' (function is undefined)
Removed calls to 'kfree_call_rcu' (function is undefined)
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Removed calls to 'fput' (function is undefined)
Removed calls to 'ldv_check_alloc_flags' (function is undefined)
Removed calls to 'ldv_after_alloc' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'dput' (function is undefined)
Defining function mount_nodev as symbolic
Removed calls to 'set_nlink' (function is undefined)
Defining function d_make_root as symbolic
Defining function printk as symbolic
Defining function find_get_pid as symbolic
Defining function get_task_pid as symbolic
Defining function fget as symbolic
Defining function debug_lockdep_rcu_enabled as symbolic
Defining function match_token as symbolic
Defining function match_int as symbolic
Defining function make_kuid as symbolic
Defining function make_kgid as symbolic
Defining function strsep as symbolic
Defining function new_inode as symbolic
Defining function current_kernel_time as symbolic
Defining function get_next_ino as symbolic
Defining function unregister_filesystem as symbolic
Defining function misc_deregister as symbolic
Defining function register_filesystem as symbolic
Defining function misc_register as symbolic
Removed calls to 'clear_inode' (function is undefined)
Defining function seq_printf as symbolic
Defining function from_kuid_munged as symbolic
Defining function from_kgid_munged as symbolic
Defining function pid_vnr as symbolic
Defining function simple_statfs as symbolic
Defining function dcache_dir_lseek as symbolic
Defining function generic_read_dir as symbolic
Defining function dcache_readdir as symbolic
Defining function dcache_dir_open as symbolic
Defining function dcache_dir_close as symbolic
Removed calls to 'might_fault' (function is undefined)
Defining function capable as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to 'complete_all' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'lockref_get' (function is undefined)
Removed calls to '__ldv_spin_lock' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to '__list_add' (function is undefined)
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)
Removed calls to 'lockdep_rcu_suspicious' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'recalc_sigpending' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Defining function task_tgid_nr_ns as symbolic
Defining function sprintf as symbolic
Defining function full_name_hash as symbolic
Defining function mutex_lock_interruptible_nested as symbolic
Defining function prepare_to_wait_event as symbolic
Defining function d_lookup as symbolic
Defining function schedule_timeout_interruptible as symbolic
Defining function have_submounts as symbolic
Defining function rcu_is_watching as symbolic
Defining function __task_pid_nr_ns as symbolic
Removed calls to 'path_get' (function is undefined)
Removed calls to 'path_put' (function is undefined)
Defining function simple_empty as symbolic
Removed calls to 'lock_set_class' (function is undefined)
Defining function _raw_spin_trylock as symbolic
Defining function d_invalidate as symbolic
Defining function follow_down_one as symbolic
Defining function may_umount_tree as symbolic
Defining function _copy_to_user as symbolic
Defining function may_umount as symbolic
Removed calls to 'd_instantiate' (function is undefined)
Removed calls to 'clear_nlink' (function is undefined)
Removed calls to 'd_drop' (function is undefined)
Removed calls to 'd_rehash' (function is undefined)
Removed calls to 'inc_nlink' (function is undefined)
Removed calls to 'drop_nlink' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to 'wait_for_completion' (function is undefined)
Defining function generic_readlink as symbolic
Removed calls to 'fd_install' (function is undefined)
Removed calls to 'put_unused_fd' (function is undefined)
Defining function kern_path_mountpoint as symbolic
Defining function follow_up as symbolic
Defining function sys_close as symbolic
Defining function get_unused_fd_flags as symbolic
Defining function dentry_open as symbolic
Defining function memdup_user as symbolic
Defining function _copy_from_user as symbolic
Defining function noop_llseek as symbolic
Defining function external_allocated_data as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'ldv_assert' (function is undefined)
Linked our definitions to these undefined functions:
  memchr
  memcmp
  strchr
  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: 0.768788814545
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 316 331 1340 8570
INFO: Starting verification
WARNING: this target does not support the llvm.returnaddress intrinsic.
WARNING: this target does not support the llvm.returnaddress intrinsic.
KLEE: WARNING ONCE: function "autofs4_fill_super" has inline asm
KLEE: WARNING ONCE: function "autofs_dev_ioctl_init" has inline asm
KLEE: WARNING ONCE: function "autofs4_root_ioctl_unlocked" has inline asm
KLEE: WARNING ONCE: function "autofs4_expire_multi" has inline asm
KLEE: WARNING ONCE: function "autofs4_wait" has inline asm
KLEE: WARNING ONCE: function "rcu_read_unlock" has inline asm
KLEE: WARNING ONCE: function "get_next_positive_dentry" has inline asm
KLEE: WARNING ONCE: function "autofs4_dir_open" has inline asm
KLEE: WARNING ONCE: function "autofs4_lookup" has inline asm
KLEE: WARNING ONCE: function "autofs4_dir_unlink" has inline asm
KLEE: WARNING ONCE: function "autofs4_dir_symlink" has inline asm
KLEE: WARNING ONCE: function "autofs4_dir_mkdir" has inline asm
KLEE: WARNING ONCE: function "autofs4_dir_rmdir" has inline asm
KLEE: WARNING ONCE: function "autofs4_d_automount" has inline asm
KLEE: WARNING ONCE: function "autofs4_d_manage" has inline asm
KLEE: WARNING ONCE: function "autofs4_follow_link" has inline asm
KLEE: WARNING ONCE: function "autofs_dev_ioctl" has inline asm
KLEE: WARNING ONCE: function "autofs_dev_ioctl_openmount" has inline asm
KLEE: WARNING ONCE: function "autofs_dev_ioctl_setpipefd" has inline asm
KLEE: WARNING ONCE: function "autofs_dev_ioctl_requester" has inline asm
KLEE: WARNING: undefined reference to variable: init_user_ns
KLEE: WARNING: Type for init_user_ns is not sized
KLEE: WARNING: Unable to find size for global variable: init_user_ns (use will result in out of bounds access)
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_d143bc97-903f-4bda-ab7b-962bc961f92d/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-XNOl3E/linux-3.14__complex_emg__linux-kernel-locking-spinlock__fs-autofs4-autofs4_true-unreach-call.cil.c:6330: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: WARNING ONCE: flushing 10568 bytes on read, may be slow and/or crash: MO163[10568] allocated at global:
KLEE: ERROR: /tmp/symbiotic-XNOl3E/linux-3.14__complex_emg__linux-kernel-locking-spinlock__fs-autofs4-autofs4_true-unreach-call.cil.c:7939: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-XNOl3E/linux-3.14__complex_emg__linux-kernel-locking-spinlock__fs-autofs4-autofs4_true-unreach-call.cil.c:6539: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-XNOl3E/linux-3.14__complex_emg__linux-kernel-locking-spinlock__fs-autofs4-autofs4_true-unreach-call.cil.c:7683: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-XNOl3E/linux-3.14__complex_emg__linux-kernel-locking-spinlock__fs-autofs4-autofs4_true-unreach-call.cil.c:6330: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
