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__drivers-net-tun_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.: 171 449 2826 15431
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.607722043991
Removed calls to 'lockdep_rcu_suspicious' (function is undefined)
Removed calls to 'add_wait_queue' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'print_hex_dump' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'kfree_skb' (function is undefined)
Removed calls to 'remove_wait_queue' (function is undefined)
Defining function default_wake_function as symbolic
Defining function skb_dequeue as symbolic
Defining function memcpy_toiovecend as symbolic
Defining function printk as symbolic
Defining function skb_copy_datagram_const_iovec as symbolic
Removed calls to 'lock_acquire' (function is undefined)
Defining function debug_lockdep_rcu_enabled as symbolic
Removed calls to 'lock_release' (function is undefined)
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 '__skb_get_hash' (function is undefined)
Removed calls to '_raw_spin_lock_bh' (function is undefined)
Removed calls to '_raw_spin_unlock_bh' (function is undefined)
Defining function memcpy_fromiovecend as symbolic
Defining function iov_pages as symbolic
Defining function zerocopy_sg_from_iovec as symbolic
Defining function skb_copy_datagram_from_iovec as symbolic
Defining function skb_partial_csum_set as symbolic
Defining function eth_type_trans as symbolic
Defining function netif_rx_ni as symbolic
Defining function round_jiffies_up as symbolic
Defining function mod_timer as symbolic
Defining function skb_flow_dissect as symbolic
Defining function sock_alloc_send_pskb as symbolic
Defining function skb_put as symbolic
Removed calls to 'might_fault' (function is undefined)
Removed calls to 'rtnl_lock' (function is undefined)
Removed calls to 'rtnl_unlock' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'ether_setup' (function is undefined)
Removed calls to 'get_random_bytes' (function is undefined)
Removed calls to 'init_timer_key' (function is undefined)
Removed calls to 'netif_carrier_on' (function is undefined)
Removed calls to 'security_tun_dev_free_security' (function is undefined)
Removed calls to 'free_netdev' (function is undefined)
Removed calls to '__module_get' (function is undefined)
Removed calls to 'module_put' (function is undefined)
Removed calls to 'netdev_update_features' (function is undefined)
Defining function make_kuid as symbolic
Defining function make_kgid as symbolic
Defining function dev_set_mac_address as symbolic
Defining function lockdep_rtnl_is_held as symbolic
Defining function sk_detach_filter as symbolic
Defining function sk_attach_filter as symbolic
Defining function crc32_le as symbolic
Defining function bitrev32 as symbolic
Defining function _copy_to_user as symbolic
Defining function __dev_get_by_name as symbolic
Defining function security_tun_dev_open as symbolic
Removed calls to '__list_del_entry' (function is undefined)
Defining function ns_capable as symbolic
Defining function security_tun_dev_create as symbolic
Defining function security_tun_dev_alloc_security as symbolic
Defining function device_create_file as symbolic
Removed calls to '__wake_up' (function is undefined)
Removed calls to 'synchronize_net' (function is undefined)
Removed calls to 'skb_queue_purge' (function is undefined)
Removed calls to 'kfree_call_rcu' (function is undefined)
Defining function del_timer_sync as symbolic
Defining function netpoll_trap as symbolic
Defining function register_netdevice as symbolic
Defining function alloc_netdev_mqs as symbolic
Defining function security_tun_dev_attach as symbolic
Defining function netif_set_real_num_tx_queues as symbolic
Defining function netif_set_real_num_rx_queues as symbolic
Defining function in_egroup_p as symbolic
Defining function security_tun_dev_attach_queue as symbolic
Removed calls to '__list_add' (function is undefined)
Removed calls to 'netif_carrier_off' (function is undefined)
Removed calls to 'unregister_netdevice_queue' (function is undefined)
Removed calls to 'sk_release_kernel' (function is undefined)
Defining function _copy_from_user as symbolic
Defining function fasync_helper as symbolic
Defining function __f_setown as symbolic
Defining function no_llseek as symbolic
Defining function do_sync_read as symbolic
Defining function seq_printf as symbolic
Removed calls to 'rtnl_link_unregister' (function is undefined)
Defining function misc_deregister as symbolic
Defining function rtnl_link_register as symbolic
Defining function misc_register as symbolic
Defining function strlcpy as symbolic
Defining function ethtool_op_get_link as symbolic
Defining function ethtool_op_get_ts_info as symbolic
Defining function eth_mac_addr as symbolic
Removed calls to 'sock_tx_timestamp' (function is undefined)
Removed calls to 'skb_tstamp_tx' (function is undefined)
Removed calls to 'skb_queue_tail' (function is undefined)
Removed calls to 'kill_fasync' (function is undefined)
Removed calls to 'skb_tx_error' (function is undefined)
Defining function sk_filter as symbolic
Defining function skb_copy_ubufs as symbolic
Defining function eth_validate_addr as symbolic
Defining function sock_recv_errqueue as symbolic
Defining function from_kgid_munged as symbolic
Defining function sprintf as symbolic
Defining function from_kuid_munged as symbolic
Defining function do_sync_write as symbolic
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'sock_init_data' (function is undefined)
Defining function sk_alloc as symbolic
Defining function external_allocated_data as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'ldv_switch_to_interrupt_context' (function is undefined)
Removed calls to 'ldv_switch_to_process_context' (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 'ldv_assert' (function is undefined)
Linked our definitions to these undefined functions:
  strcpy
  __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.582498788834
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 269 379 1373 7897
INFO: Starting verification
KLEE: WARNING ONCE: function "tun_chr_aio_read" has inline asm
KLEE: WARNING ONCE: function "__tun_get" has inline asm
KLEE: WARNING ONCE: function "tun_do_read" has inline asm
KLEE: WARNING ONCE: function "rcu_read_lock" has inline asm
KLEE: WARNING ONCE: function "rcu_read_unlock" has inline asm
KLEE: WARNING ONCE: function "tun_chr_aio_write" has inline asm
KLEE: WARNING ONCE: function "tun_get_user" has inline asm
KLEE: WARNING ONCE: function "__tun_chr_ioctl" has inline asm
KLEE: WARNING ONCE: function "tun_attach" has inline asm
KLEE: WARNING ONCE: function "__tun_detach" has inline asm
KLEE: WARNING ONCE: function "tun_detach_all" has inline asm
KLEE: WARNING ONCE: function "tun_free_netdev" has inline asm
KLEE: WARNING ONCE: function "tun_chr_fasync" has inline asm
KLEE: WARNING ONCE: function "tun_chr_poll" has inline asm
KLEE: WARNING ONCE: function "tun_chr_show_fdinfo" has inline asm
KLEE: WARNING ONCE: function "tun_net_open" has inline asm
KLEE: WARNING ONCE: function "tun_net_xmit" has inline asm
KLEE: WARNING ONCE: function "tun_net_close" has inline asm
KLEE: WARNING ONCE: function "tun_recvmsg" has inline asm
KLEE: WARNING ONCE: function "tun_sendmsg" has inline asm
KLEE: WARNING ONCE: function "tun_show_group" has inline asm
KLEE: WARNING ONCE: function "tun_show_owner" has inline asm
KLEE: WARNING ONCE: function "tun_chr_open" has inline asm
KLEE: WARNING ONCE: function "ldv_dummy_resourceless_instance_callback_1_18" has inline asm
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_df15c071-d094-4ea8-8b50-44a0fd534898/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
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: ERROR: /tmp/symbiotic-PfCxG4/linux-3.14__complex_emg__linux-kernel-locking-spinlock__drivers-net-tun_true-unreach-call.cil.c:12406: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: flushing 5416 bytes on read, may be slow and/or crash: MO168[5416] allocated at global:init_net
KLEE: ERROR: /tmp/symbiotic-PfCxG4/linux-3.14__complex_emg__linux-kernel-locking-spinlock__drivers-net-tun_true-unreach-call.cil.c:12406: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-PfCxG4/linux-3.14__complex_emg__linux-kernel-locking-spinlock__drivers-net-tun_true-unreach-call.cil.c:5900: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 11330 states (over memory cap)
KLEE: WARNING: killing 10219 states (over memory cap)
KLEE: WARNING: killing 10400 states (over memory cap)
KLEE: WARNING: killing 10283 states (over memory cap)
KLEE: WARNING: killing 10364 states (over memory cap)
KLEE: WARNING: killing 19306 states (over memory cap)
KLEE: WARNING: killing 10600 states (over memory cap)
KLEE: WARNING: killing 9894 states (over memory cap)
KLEE: WARNING: killing 9873 states (over memory cap)
KLEE: WARNING: killing 19336 states (over memory cap)
KLEE: WARNING: killing 9923 states (over memory cap)
KLEE: WARNING: killing 10001 states (over memory cap)
KLEE: WARNING: killing 19507 states (over memory cap)
KLEE: WARNING: killing 10726 states (over memory cap)
KLEE: WARNING: killing 10518 states (over memory cap)
KLEE: WARNING: killing 10599 states (over memory cap)
KLEE: WARNING: killing 10388 states (over memory cap)
KLEE: WARNING: killing 11242 states (over memory cap)
KLEE: WARNING: killing 10844 states (over memory cap)
KLEE: WARNING: killing 11024 states (over memory cap)
KLEE: WARNING: killing 10721 states (over memory cap)
KLEE: WARNING: killing 11281 states (over memory cap)
KLEE: WARNING: killing 11074 states (over memory cap)
KLEE: WARNING: killing 11249 states (over memory cap)
KLEE: WARNING: killing 10562 states (over memory cap)
KLEE: WARNING: killing 10743 states (over memory cap)
KLEE: WARNING: killing 10727 states (over memory cap)
KLEE: WARNING: killing 10524 states (over memory cap)
KLEE: WARNING: killing 10794 states (over memory cap)
KLEE: WARNING: killing 11160 states (over memory cap)
KLEE: WARNING: killing 10866 states (over memory cap)
KLEE: WARNING: killing 11134 states (over memory cap)
KLEE: WARNING: killing 11312 states (over memory cap)
KLEE: WARNING: killing 10260 states (over memory cap)
KLEE: WARNING: killing 10343 states (over memory cap)
KLEE: WARNING: killing 10419 states (over memory cap)
KLEE: WARNING: killing 10687 states (over memory cap)
KLEE: WARNING: killing 10961 states (over memory cap)
KLEE: WARNING: killing 10099 states (over memory cap)
KLEE: WARNING: killing 10554 states (over memory cap)
KLEE: WARNING: killing 10545 states (over memory cap)
KLEE: WARNING: killing 10531 states (over memory cap)
KLEE: WARNING: killing 10614 states (over memory cap)
KLEE: WARNING: killing 10507 states (over memory cap)
KLEE: WARNING: killing 10497 states (over memory cap)
KLEE: WARNING: killing 10671 states (over memory cap)
KLEE: WARNING: killing 10659 states (over memory cap)
KLEE: WARNING: killing 10551 states (over memory cap)
KLEE: WARNING: killing 10258 states (over memory cap)
KLEE: WARNING: killing 10995 states (over memory cap)
KLEE: WARNING: killing 10330 states (over memory cap)
KLEE: WARNING: killing 10876 states (over memory cap)
KLEE: WARNING: killing 10956 states (over memory cap)
KLEE: WARNING: killing 10573 states (over memory cap)
KLEE: WARNING: killing 10840 states (over memory cap)
KLEE: WARNING: killing 10546 states (over memory cap)
KLEE: WARNING: killing 10722 states (over memory cap)
KLEE: WARNING: killing 10250 states (over memory cap)
KLEE: WARNING: killing 9961 states (over memory cap)
KLEE: WARNING: killing 10224 states (over memory cap)
KLEE: WARNING: killing 10303 states (over memory cap)
KLEE: WARNING: killing 10478 states (over memory cap)
KLEE: WARNING: killing 10283 states (over memory cap)
KLEE: WARNING: killing 11006 states (over memory cap)
KLEE: WARNING: killing 10810 states (over memory cap)
KLEE: WARNING: killing 10527 states (over memory cap)
KLEE: WARNING: killing 10421 states (over memory cap)
KLEE: WARNING: killing 10688 states (over memory cap)
KLEE: WARNING: killing 11134 states (over memory cap)
KLEE: WARNING: killing 10028 states (over memory cap)
KLEE: WARNING: killing 10563 states (over memory cap)
KLEE: WARNING: killing 10550 states (over memory cap)
KLEE: WARNING: killing 10453 states (over memory cap)
KLEE: WARNING: killing 10345 states (over memory cap)
KLEE: WARNING: killing 10428 states (over memory cap)
KLEE: WARNING: killing 10781 states (over memory cap)
KLEE: WARNING: killing 10499 states (over memory cap)
KLEE: WARNING: killing 10306 states (over memory cap)
KLEE: WARNING: killing 10297 states (over memory cap)
KLEE: WARNING: killing 10733 states (over memory cap)
KLEE: WARNING: killing 10636 states (over memory cap)
KLEE: WARNING: killing 10535 states (over memory cap)
KLEE: WARNING: killing 10701 states (over memory cap)
KLEE: WARNING: killing 10690 states (over memory cap)
KLEE: WARNING: killing 10863 states (over memory cap)
KLEE: WARNING: killing 10400 states (over memory cap)
KLEE: WARNING: killing 10388 states (over memory cap)
KLEE: WARNING: killing 10824 states (over memory cap)
KLEE: WARNING: killing 10551 states (over memory cap)
KLEE: WARNING: killing 10274 states (over memory cap)
KLEE: WARNING: killing 10886 states (over memory cap)
KLEE: WARNING: killing 10522 states (over memory cap)
KLEE: WARNING: killing 10866 states (over memory cap)
KLEE: WARNING: killing 10585 states (over memory cap)
KLEE: WARNING: killing 10399 states (over memory cap)
KLEE: WARNING: killing 10299 states (over memory cap)
KLEE: WARNING: killing 10203 states (over memory cap)
KLEE: WARNING: killing 10457 states (over memory cap)
KLEE: WARNING: killing 10450 states (over memory cap)
KLEE: WARNING: killing 10791 states (over memory cap)
KLEE: WARNING: killing 10697 states (over memory cap)
KLEE: WARNING: killing 10511 states (over memory cap)
KLEE: WARNING: killing 10325 states (over memory cap)
KLEE: WARNING: killing 10670 states (over memory cap)
KLEE: WARNING: killing 10656 states (over memory cap)
KLEE: WARNING: killing 10299 states (over memory cap)
KLEE: WARNING: killing 10464 states (over memory cap)
KLEE: WARNING: killing 10711 states (over memory cap)
KLEE: WARNING: killing 10442 states (over memory cap)
KLEE: WARNING: killing 10779 states (over memory cap)
KLEE: WARNING: killing 10417 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-PfCxG4/linux-3.14__complex_emg__linux-kernel-locking-spinlock__drivers-net-tun_true-unreach-call.cil.c:5900: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 10499 states (over memory cap)
KLEE: WARNING: killing 10404 states (over memory cap)
KLEE: WARNING: killing 10304 states (over memory cap)
KLEE: WARNING: killing 10465 states (over memory cap)
KLEE: WARNING: killing 10633 states (over memory cap)
KLEE: WARNING: killing 10273 states (over memory cap)
KLEE: WARNING: killing 10352 states (over memory cap)
KLEE: WARNING: killing 10688 states (over memory cap)
KLEE: WARNING: killing 10769 states (over memory cap)
KLEE: WARNING: killing 10585 states (over memory cap)
KLEE: WARNING: killing 10488 states (over memory cap)
KLEE: WARNING: killing 10739 states (over memory cap)
KLEE: WARNING: killing 10642 states (over memory cap)
KLEE: WARNING: killing 10546 states (over memory cap)
KLEE: WARNING: killing 10705 states (over memory cap)
KLEE: WARNING: killing 10526 states (over memory cap)
KLEE: WARNING: killing 10253 states (over memory cap)
KLEE: WARNING: killing 10676 states (over memory cap)
KLEE: WARNING: killing 10496 states (over memory cap)
KLEE: WARNING: killing 10142 states (over memory cap)
KLEE: WARNING: killing 10996 states (over memory cap)
KLEE: WARNING: killing 10816 states (over memory cap)
KLEE: WARNING: killing 10292 states (over memory cap)
KLEE: WARNING: killing 10623 states (over memory cap)
KLEE: WARNING: killing 10614 states (over memory cap)
KLEE: WARNING: killing 10517 states (over memory cap)
KLEE: WARNING: killing 10170 states (over memory cap)
KLEE: WARNING: killing 11014 states (over memory cap)
KLEE: WARNING: killing 10836 states (over memory cap)
KLEE: WARNING: killing 10573 states (over memory cap)
KLEE: WARNING: killing 10473 states (over memory cap)
KLEE: WARNING: killing 10122 states (over memory cap)
KLEE: WARNING: killing 10710 states (over memory cap)
KLEE: WARNING: killing 10363 states (over memory cap)
KLEE: WARNING: killing 10351 states (over memory cap)
KLEE: WARNING: killing 10088 states (over memory cap)
KLEE: WARNING: killing 10669 states (over memory cap)
KLEE: WARNING: killing 10662 states (over memory cap)
KLEE: WARNING: killing 10484 states (over memory cap)
KLEE: WARNING: killing 10391 states (over memory cap)
KLEE: WARNING: killing 10721 states (over memory cap)
KLEE: WARNING: killing 10460 states (over memory cap)
KLEE: WARNING: killing 10449 states (over memory cap)
KLEE: WARNING: killing 10612 states (over memory cap)
KLEE: WARNING: killing 10265 states (over memory cap)
KLEE: WARNING: killing 10342 states (over memory cap)
KLEE: WARNING: killing 10330 states (over memory cap)
KLEE: WARNING: killing 10574 states (over memory cap)
KLEE: WARNING: killing 10565 states (over memory cap)
KLEE: WARNING: killing 10388 states (over memory cap)
KLEE: WARNING: killing 10548 states (over memory cap)
KLEE: WARNING: killing 10623 states (over memory cap)
KLEE: WARNING: killing 10530 states (over memory cap)
KLEE: WARNING: killing 10767 states (over memory cap)
KLEE: WARNING: killing 10342 states (over memory cap)
KLEE: WARNING: killing 10497 states (over memory cap)
KLEE: WARNING: killing 10573 states (over memory cap)
KLEE: WARNING: killing 10148 states (over memory cap)
KLEE: WARNING: killing 10806 states (over memory cap)
KLEE: WARNING: killing 10880 states (over memory cap)
KLEE: WARNING: killing 10458 states (over memory cap)
KLEE: WARNING: killing 10450 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-PfCxG4/linux-3.14__complex_emg__linux-kernel-locking-spinlock__drivers-net-tun_true-unreach-call.cil.c:5900: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 10354 states (over memory cap)
KLEE: WARNING: killing 11009 states (over memory cap)
KLEE: WARNING: killing 10668 states (over memory cap)
KLEE: WARNING: killing 9745 states (over memory cap)
KLEE: WARNING: killing 10149 states (over memory cap)
KLEE: WARNING: killing 10635 states (over memory cap)
KLEE: WARNING: killing 10713 states (over memory cap)
KLEE: WARNING: killing 10700 states (over memory cap)
KLEE: WARNING: killing 10612 states (over memory cap)
KLEE: WARNING: killing 10434 states (over memory cap)
KLEE: WARNING: killing 10924 states (over memory cap)
KLEE: WARNING: killing 10502 states (over memory cap)
KLEE: WARNING: killing 10330 states (over memory cap)
KLEE: WARNING: killing 10235 states (over memory cap)
KLEE: WARNING: killing 10638 states (over memory cap)
KLEE: WARNING: killing 10301 states (over memory cap)
KLEE: WARNING: killing 10211 states (over memory cap)
KLEE: WARNING: killing 10447 states (over memory cap)
KLEE: WARNING: killing 10432 states (over memory cap)
KLEE: WARNING: killing 10835 states (over memory cap)
KLEE: WARNING: killing 10504 states (over memory cap)
KLEE: WARNING: killing 10573 states (over memory cap)
KLEE: WARNING: killing 10323 states (over memory cap)
KLEE: WARNING: killing 10309 states (over memory cap)
KLEE: WARNING: killing 10546 states (over memory cap)
KLEE: WARNING: killing 10455 states (over memory cap)
KLEE: WARNING: killing 10452 states (over memory cap)
KLEE: WARNING: killing 10281 states (over memory cap)
KLEE: WARNING: killing 10352 states (over memory cap)
KLEE: WARNING: killing 10340 states (over memory cap)
KLEE: WARNING: killing 10741 states (over memory cap)
KLEE: WARNING: killing 10728 states (over memory cap)
KLEE: WARNING: killing 10723 states (over memory cap)
KLEE: WARNING: killing 10555 states (over memory cap)
KLEE: WARNING: killing 10385 states (over memory cap)
KLEE: WARNING: killing 10943 states (over memory cap)
KLEE: WARNING: killing 10288 states (over memory cap)
KLEE: WARNING: killing 10438 states (over memory cap)
KLEE: WARNING: killing 10511 states (over memory cap)
KLEE: WARNING: killing 10181 states (over memory cap)
