bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-net--unix--unix.ko-entry_point_false-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.: 101 281 2031 13273
Removed infinite loop in unix_notinflight
Removed infinite loop in unix_inflight
Removed infinite loop in unix_gc
Removed infinite loop in scan_children
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.545309782028
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function seq_puts as symbolic
Defining function sock_i_ino as symbolic
Defining function seq_printf as symbolic
Defining function seq_putc as symbolic
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'kfree_skb' (function is undefined)
Removed calls to 'path_get' (function is undefined)
Removed calls to 'put_pid' (function is undefined)
Removed calls to 'skb_free_datagram' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Removed calls to '_raw_write_lock_bh' (function is undefined)
Removed calls to 'security_sock_graft' (function is undefined)
Removed calls to '_raw_write_unlock_bh' (function is undefined)
Removed calls to 'might_fault' (function is undefined)
Defining function sock_no_setsockopt as symbolic
Defining function sock_no_getsockopt as symbolic
Removed calls to 'skb_queue_tail' (function is undefined)
Removed calls to 'prepare_to_wait' (function is undefined)
Removed calls to 'debug_check_no_locks_held' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to 'skb_unlink' (function is undefined)
Removed calls to 'consume_skb' (function is undefined)
Defining function sock_no_mmap as symbolic
Defining function sock_no_sendpage as symbolic
Defining function mutex_lock_interruptible_nested as symbolic
Defining function skb_copy_datagram_iovec as symbolic
Defining function scm_fp_dup as symbolic
Removed calls to 'security_release_secctx' (function is undefined)
Removed calls to 'scm_detach_fds' (function is undefined)
Removed calls to '__scm_destroy' (function is undefined)
Defining function debug_lockdep_rcu_enabled as symbolic
Defining function from_kuid_munged as symbolic
Defining function from_kgid_munged as symbolic
Defining function put_cmsg as symbolic
Defining function security_secid_to_secctx as symbolic
Removed calls to '__list_del_entry' (function is undefined)
Defining function pid_vnr as symbolic
Defining function autoremove_wake_function as symbolic
Defining function schedule_timeout as symbolic
Defining function __refrigerator as symbolic
Defining function freezing_slow_path as symbolic
Defining function rcu_is_watching as symbolic
Defining function rcu_lockdep_current_cpu_online as symbolic
Defining function lock_is_held as symbolic
Removed calls to 'schedule' (function is undefined)
Defining function sock_alloc_send_pskb as symbolic
Defining function skb_put as symbolic
Defining function skb_copy_datagram_from_iovec as symbolic
Defining function send_sig as symbolic
Removed calls to 'sock_wfree' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Defining function __scm_send as symbolic
Defining function security_socket_getpeersec_dgram as symbolic
Removed calls to 'list_del' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Defining function prepare_to_wait_event as symbolic
Removed calls to 'sk_free' (function is undefined)
Defining function sock_wake_async as symbolic
Removed calls to '__put_cred' (function is undefined)
Removed calls to '__invalid_creds' (function is undefined)
Defining function creds_are_invalid as symbolic
Defining function skb_recv_datagram as symbolic
Removed calls to 'sock_init_data' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to '__local_bh_disable_ip' (function is undefined)
Removed calls to 'sock_prot_inuse_add' (function is undefined)
Removed calls to '__local_bh_enable_ip' (function is undefined)
Defining function sock_wmalloc as symbolic
Removed calls to 'touch_atime' (function is undefined)
Removed calls to 'path_put' (function is undefined)
Removed calls to 'prepare_to_wait_exclusive' (function is undefined)
Defining function security_unix_stream_connect as symbolic
Defining function skb_dequeue as symbolic
Defining function kern_path as symbolic
Defining function inode_permission as symbolic
Defining function get_max_files as symbolic
Defining function sk_alloc as symbolic
Removed calls to 'lock_acquire' (function is undefined)
Removed calls to 'lockdep_rcu_suspicious' (function is undefined)
Removed calls to '__wake_up_sync_key' (function is undefined)
Removed calls to 'lock_release' (function is undefined)
Removed calls to 'skb_queue_purge' (function is undefined)
Defining function printk as symbolic
Defining function csum_partial as symbolic
Defining function sock_no_accept as symbolic
Defining function sock_no_listen as symbolic
Removed calls to '__sock_recv_timestamp' (function is undefined)
Defining function __skb_recv_datagram as symbolic
Defining function sk_filter as symbolic
Defining function security_unix_may_send as symbolic
Defining function ktime_get_real as symbolic
Defining function seq_lseek as symbolic
Defining function seq_read as symbolic
Defining function seq_release_net as symbolic
Defining function seq_open_net as symbolic
Removed calls to 'unregister_net_sysctl_table' (function is undefined)
Removed calls to 'remove_proc_entry' (function is undefined)
Defining function proc_create_data as symbolic
Defining function kmemdup as symbolic
Defining function register_net_sysctl as symbolic
Defining function proc_dointvec as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'sock_unregister' (function is undefined)
Removed calls to 'proto_unregister' (function is undefined)
Removed calls to 'unregister_pernet_subsys' (function is undefined)
Removed calls to 'ldv_check_final_state' (function is undefined)
Defining function proto_register as symbolic
Defining function sock_register as symbolic
Defining function register_pernet_subsys as symbolic
Defining function kmem_cache_alloc as symbolic
Defining function pskb_expand_head as symbolic
Defining function skb_clone as symbolic
Defining function skb_copy as symbolic
Defining function __netdev_alloc_skb as symbolic
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  memcmp
  strlen
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_assume
  __VERIFIER_calloc0
  __VERIFIER_error
  __VERIFIER_exit
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
  __VERIFIER_nondet_loff_t_named
  __VERIFIER_nondet_pointer_named
  __VERIFIER_nondet_size_t_named
  __VERIFIER_nondet_uint_named
  __VERIFIER_nondet_ulong_named
INFO: After-slicing optimizations and preparation time: 0.546521902084
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 270 200 1161 7328
INFO: Starting verification
KLEE: WARNING ONCE: function "unix_peer_get" has inline asm
KLEE: WARNING ONCE: function "unix_stream_connect" has inline asm
KLEE: WARNING ONCE: function "unix_socketpair" has inline asm
KLEE: WARNING ONCE: function "unix_accept" has inline asm
KLEE: WARNING ONCE: function "unix_getname" has inline asm
KLEE: WARNING ONCE: function "unix_poll" has inline asm
KLEE: WARNING ONCE: function "unix_ioctl" has inline asm
KLEE: WARNING ONCE: function "unix_shutdown" has inline asm
KLEE: WARNING ONCE: function "unix_stream_sendmsg" has inline asm
KLEE: WARNING ONCE: function "unix_stream_recvmsg" has inline asm
KLEE: WARNING ONCE: function "scm_recv" has inline asm
KLEE: WARNING ONCE: function "unix_notinflight" has inline asm
KLEE: WARNING ONCE: function "unix_scm_to_skb" has inline asm
KLEE: WARNING ONCE: function "maybe_add_creds" has inline asm
KLEE: WARNING ONCE: function "unix_inflight" has inline asm
KLEE: WARNING ONCE: function "unix_gc" has inline asm
KLEE: WARNING ONCE: function "dec_inflight" has inline asm
KLEE: WARNING ONCE: function "scan_children" has inline asm
KLEE: WARNING ONCE: function "inc_inflight_move_tail" has inline asm
KLEE: WARNING ONCE: function "inc_inflight" has inline asm
KLEE: WARNING ONCE: function "sock_put" has inline asm
KLEE: WARNING ONCE: function "init_peercred" has inline asm
KLEE: WARNING ONCE: function "put_cred" has inline asm
KLEE: WARNING ONCE: function "unix_mkname" has inline asm
KLEE: WARNING ONCE: function "unix_create1" has inline asm
KLEE: WARNING ONCE: function "unix_release_sock" has inline asm
KLEE: WARNING ONCE: function "unix_find_other" has inline asm
KLEE: WARNING ONCE: function "unix_wait_for_peer" has inline asm
KLEE: WARNING ONCE: function "unix_write_space" has inline asm
KLEE: WARNING ONCE: function "unix_sock_destructor" has inline asm
KLEE: WARNING ONCE: function "unix_dgram_connect" has inline asm
KLEE: WARNING ONCE: function "unix_dgram_poll" has inline asm
KLEE: WARNING ONCE: function "unix_dgram_sendmsg" has inline asm
KLEE: WARNING ONCE: function "unix_dgram_recvmsg" has inline asm
KLEE: WARNING ONCE: function "unix_dgram_disconnected" has inline asm
KLEE: WARNING ONCE: function "unix_seqpacket_sendmsg" 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: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_baee2f1e-e46d-484f-ba78-b857d9c9c07b/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 2918 states (over memory cap)
KLEE: WARNING: killing 3501 states (over memory cap)
KLEE: WARNING: killing 3088 states (over memory cap)
KLEE: WARNING: killing 3385 states (over memory cap)
KLEE: WARNING: killing 4780 states (over memory cap)
KLEE: WARNING: killing 5515 states (over memory cap)
KLEE: WARNING: killing 4933 states (over memory cap)
KLEE: WARNING: killing 4661 states (over memory cap)
KLEE: WARNING: killing 4698 states (over memory cap)
KLEE: WARNING: killing 4463 states (over memory cap)
KLEE: WARNING: killing 4863 states (over memory cap)
KLEE: WARNING: killing 4848 states (over memory cap)
KLEE: WARNING: killing 5303 states (over memory cap)
KLEE: WARNING: killing 5237 states (over memory cap)
KLEE: WARNING: killing 5613 states (over memory cap)
KLEE: WARNING: killing 5469 states (over memory cap)
KLEE: WARNING: killing 5219 states (over memory cap)
KLEE: WARNING: killing 5542 states (over memory cap)
KLEE: WARNING: killing 5346 states (over memory cap)
KLEE: WARNING: killing 5288 states (over memory cap)
KLEE: WARNING: killing 5123 states (over memory cap)
KLEE: WARNING: killing 4983 states (over memory cap)
KLEE: WARNING: killing 5037 states (over memory cap)
KLEE: WARNING: killing 5036 states (over memory cap)
KLEE: WARNING: killing 5033 states (over memory cap)
KLEE: WARNING: killing 5169 states (over memory cap)
KLEE: WARNING: killing 5117 states (over memory cap)
KLEE: WARNING: killing 5199 states (over memory cap)
KLEE: WARNING: killing 5529 states (over memory cap)
KLEE: WARNING: killing 4959 states (over memory cap)
KLEE: WARNING: killing 5369 states (over memory cap)
KLEE: WARNING: killing 5265 states (over memory cap)
KLEE: WARNING: killing 5321 states (over memory cap)
KLEE: WARNING: killing 5489 states (over memory cap)
KLEE: WARNING: killing 5135 states (over memory cap)
KLEE: WARNING: killing 5438 states (over memory cap)
KLEE: WARNING: killing 5032 states (over memory cap)
KLEE: WARNING: killing 5114 states (over memory cap)
KLEE: WARNING: killing 5200 states (over memory cap)
KLEE: WARNING: killing 5420 states (over memory cap)
KLEE: WARNING: killing 5232 states (over memory cap)
KLEE: WARNING: killing 5342 states (over memory cap)
KLEE: WARNING: killing 5509 states (over memory cap)
KLEE: WARNING: killing 5344 states (over memory cap)
KLEE: WARNING: killing 5538 states (over memory cap)
KLEE: WARNING: killing 5538 states (over memory cap)
KLEE: WARNING: killing 5375 states (over memory cap)
KLEE: WARNING: killing 5623 states (over memory cap)
KLEE: WARNING: killing 5733 states (over memory cap)
KLEE: WARNING: killing 5102 states (over memory cap)
KLEE: WARNING: killing 5815 states (over memory cap)
KLEE: WARNING: killing 5843 states (over memory cap)
KLEE: WARNING: killing 5980 states (over memory cap)
KLEE: WARNING: killing 6723 states (over memory cap)
KLEE: WARNING: killing 6643 states (over memory cap)
KLEE: WARNING: killing 6476 states (over memory cap)
KLEE: WARNING: killing 6174 states (over memory cap)
KLEE: WARNING: killing 6996 states (over memory cap)
KLEE: WARNING: killing 7159 states (over memory cap)
KLEE: WARNING: killing 7572 states (over memory cap)
KLEE: WARNING: killing 8366 states (over memory cap)
KLEE: WARNING: killing 8914 states (over memory cap)
KLEE: WARNING: killing 8969 states (over memory cap)
KLEE: WARNING: killing 9049 states (over memory cap)
KLEE: WARNING: killing 9102 states (over memory cap)
KLEE: WARNING: killing 9616 states (over memory cap)
KLEE: WARNING: killing 9808 states (over memory cap)
KLEE: WARNING: killing 10354 states (over memory cap)
KLEE: WARNING: killing 10017 states (over memory cap)
KLEE: WARNING: killing 10152 states (over memory cap)
KLEE: WARNING: killing 10998 states (over memory cap)
KLEE: WARNING: killing 10770 states (over memory cap)
KLEE: WARNING: killing 10815 states (over memory cap)
KLEE: WARNING: killing 11788 states (over memory cap)
KLEE: WARNING: killing 11428 states (over memory cap)
KLEE: WARNING: killing 12160 states (over memory cap)
KLEE: WARNING: killing 11548 states (over memory cap)
KLEE: WARNING: killing 11596 states (over memory cap)
KLEE: WARNING: killing 11640 states (over memory cap)
KLEE: WARNING: killing 12425 states (over memory cap)
KLEE: WARNING: killing 12090 states (over memory cap)
KLEE: WARNING: killing 11944 states (over memory cap)
KLEE: WARNING: killing 11962 states (over memory cap)
KLEE: WARNING: killing 12472 states (over memory cap)
KLEE: WARNING: killing 12548 states (over memory cap)
KLEE: WARNING: killing 12590 states (over memory cap)
KLEE: WARNING: killing 12745 states (over memory cap)
KLEE: WARNING: killing 12115 states (over memory cap)
KLEE: WARNING: killing 12432 states (over memory cap)
KLEE: WARNING: killing 12802 states (over memory cap)
KLEE: WARNING: killing 12518 states (over memory cap)
KLEE: WARNING: killing 12509 states (over memory cap)
KLEE: WARNING: killing 12501 states (over memory cap)
KLEE: WARNING: killing 12270 states (over memory cap)
KLEE: WARNING: killing 13044 states (over memory cap)
KLEE: WARNING: killing 13121 states (over memory cap)
KLEE: WARNING: killing 12843 states (over memory cap)
KLEE: WARNING: killing 12617 states (over memory cap)
KLEE: WARNING: killing 12312 states (over memory cap)
KLEE: WARNING: killing 12437 states (over memory cap)
KLEE: WARNING: killing 11991 states (over memory cap)
KLEE: WARNING: killing 13091 states (over memory cap)
KLEE: WARNING: killing 13167 states (over memory cap)
KLEE: WARNING: killing 12942 states (over memory cap)
