bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-net--netfilter--ipvs--ip_vs.ko-ldv_main1_sequence_infinite_withcheck_stateful.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.: 523 804 7536 55154
Removed infinite loop in ip_vs_dbg_addr___3
Removed infinite loop in skb_net___3
Removed infinite loop in skb_net___0
Removed infinite loop in skb_net___1
Removed infinite loop in ip_vs_dbg_addr
Removed infinite loop in ip_vs_dbg_addr___0
Removed infinite loop in ip_vs_dbg_addr___1
Removed infinite loop in skb_net___4
Removed infinite loop in ip_vs_dbg_addr___4
Removed infinite loop in ip_vs_dbg_addr___5
Removed infinite loop in skb_net___5
Removed infinite loop in net_generic
Removed infinite loop in __skb_pull
Removed infinite loop in do_ip_vs_get_ctl
Removed infinite loop in skb_sknet
Removed infinite loop in ip_vs_dbg_addr___2
Removed infinite loop in skb_net
Removed infinite loop in skb_net___2
INFO: Compilation, preparation and instrumentation time: 1.86486887932
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to '_raw_spin_lock_bh' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to '_raw_spin_unlock_bh' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Defining function printk as symbolic
Defining function snprintf as symbolic
Defining function try_module_get as symbolic
Defining function skb_checksum as symbolic
Defining function csum_ipv6_magic as symbolic
Defining function net_ratelimit as symbolic
Defining function skb_copy_bits as symbolic
Defining function skb_make_writable as symbolic
Defining function csum_partial as symbolic
Removed calls to '_raw_read_lock' (function is undefined)
Removed calls to '_raw_read_unlock' (function is undefined)
Removed calls to 'icmpv6_send' (function is undefined)
Removed calls to 'icmp_send' (function is undefined)
Defining function inet_addr_type as symbolic
Removed calls to 'init_timer_key' (function is undefined)
Removed calls to '__module_get' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function rcu_read_lock_bh_held as symbolic
Defining function debug_lockdep_rcu_enabled as symbolic
Defining function rcu_is_cpu_idle as symbolic
Defining function rcu_lockdep_current_cpu_online as symbolic
Defining function lock_is_held as symbolic
Defining function mod_timer as symbolic
Removed calls to 'module_put' (function is undefined)
Removed calls to 'kmem_cache_free' (function is undefined)
Removed calls to '_raw_write_lock' (function is undefined)
Removed calls to '_raw_write_unlock' (function is undefined)
Removed calls to 'ip_send_check' (function is undefined)
Removed calls to 'dst_release' (function is undefined)
Removed calls to 'kfree_skb' (function is undefined)
Removed calls to 'consume_skb' (function is undefined)
Removed calls to '__ip_select_ident' (function is undefined)
Defining function nf_hook_slow as symbolic
Removed calls to 'nf_conntrack_destroy' (function is undefined)
Defining function skb_clone as symbolic
Defining function ip_route_output_flow as symbolic
Defining function skb_realloc_headroom as symbolic
Defining function skb_push as symbolic
Removed calls to 'nf_ct_deliver_cached_events' (function is undefined)
Defining function ip_local_out as symbolic
Defining function __nf_conntrack_confirm as symbolic
Removed calls to 'lock_acquire' (function is undefined)
Removed calls to 'lockdep_rcu_suspicious' (function is undefined)
Removed calls to 'lock_release' (function is undefined)
Removed calls to 'nf_conntrack_alter_reply' (function is undefined)
Defining function ip_route_input_noref as symbolic
Defining function pskb_expand_head as symbolic
Defining function ip6_route_output as symbolic
Defining function ipv6_dev_get_saddr as symbolic
Defining function xfrm_lookup as symbolic
Defining function ip6_local_out as symbolic
Defining function sprintf as symbolic
Defining function del_timer as symbolic
Defining function strnlen as symbolic
Defining function schedule_delayed_work as symbolic
Defining function wake_up_process as symbolic
Defining function nf_conntrack_find_get as symbolic
Defining function kmem_cache_alloc as symbolic
Defining function __ipv6_addr_type as symbolic
Defining function kmemdup as symbolic
Defining function crc32c 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 '_raw_read_unlock_bh' (function is undefined)
Removed calls to '_raw_read_lock_bh' (function is undefined)
Defining function seq_puts as symbolic
Defining function seq_printf as symbolic
Removed calls to 'proc_net_remove' (function is undefined)
Removed calls to '_raw_write_unlock_bh' (function is undefined)
Removed calls to '_raw_write_lock_bh' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'free_percpu' (function is undefined)
Removed calls to 'unregister_net_sysctl_table' (function is undefined)
Defining function del_timer_sync as symbolic
Defining function cancel_delayed_work_sync as symbolic
Defining function cancel_work_sync as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to '__rwlock_init' (function is undefined)
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Defining function proc_net_fops_create as symbolic
Defining function __alloc_percpu as symbolic
Defining function nr_free_buffer_pages as symbolic
Defining function register_net_sysctl as symbolic
Removed calls to 'si_meminfo' (function is undefined)
Removed calls to 'local_bh_disable' (function is undefined)
Removed calls to 'local_bh_enable' (function is undefined)
Defining function prandom_u32 as symbolic
Defining function find_next_bit as symbolic
Defining function kthread_stop as symbolic
Defining function ipv6_find_hdr as symbolic
Removed calls to 'ipv4_update_pmtu' (function is undefined)
Defining function ip_defrag as symbolic
Defining function ip6_route_me_harder as symbolic
Defining function ip_route_me_harder as symbolic
Defining function single_release_net as symbolic
Defining function single_open_net as symbolic
Defining function proc_dointvec as symbolic
Defining function proc_dointvec_jiffies as symbolic
Defining function proc_dointvec_minmax as symbolic
Removed calls to 'might_fault' (function is undefined)
Defining function ns_capable as symbolic
Defining function strlcpy as symbolic
Defining function mutex_lock_interruptible as symbolic
Defining function _copy_to_user as symbolic
Defining function _copy_from_user as symbolic
Removed calls to 'lock_sock_nested' (function is undefined)
Removed calls to 'release_sock' (function is undefined)
Removed calls to 'sk_release_kernel' (function is undefined)
Defining function __request_module as symbolic
Removed calls to 'prepare_to_wait' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Defining function kthread_create_on_node as symbolic
Defining function sock_create_kern as symbolic
Removed calls to '__put_net' (function is undefined)
Defining function __dev_get_by_name as symbolic
Defining function ip_mc_join_group as symbolic
Defining function inet_select_addr as symbolic
Defining function kthread_should_stop as symbolic
Defining function autoremove_wake_function as symbolic
Defining function kernel_recvmsg as symbolic
Defining function schedule_timeout as symbolic
Defining function kernel_sendmsg as symbolic
Removed calls to 'skb_trim' (function is undefined)
Defining function genlmsg_put as symbolic
Defining function nla_put as symbolic
Defining function nla_parse as symbolic
Defining function nla_memcpy as symbolic
Defining function netlink_unicast as symbolic
Defining function __alloc_skb as symbolic
Defining function seq_putc as symbolic
Removed calls to 'vfree' (function is undefined)
Removed calls to 'get_random_bytes' (function is undefined)
Defining function vmalloc as symbolic
Defining function kmem_cache_create as symbolic
Removed calls to 'kmem_cache_destroy' (function is undefined)
Removed calls to 'ldv_handler_precall' (function is undefined)
Removed calls to 'ldv_check_return_value' (function is undefined)
Defining function mutex_trylock as symbolic
Removed calls to 'nf_unregister_hooks' (function is undefined)
Removed calls to 'unregister_pernet_device' (function is undefined)
Removed calls to 'unregister_pernet_subsys' (function is undefined)
Removed calls to 'nf_unregister_sockopt' (function is undefined)
Defining function unregister_netdevice_notifier as symbolic
Defining function genl_unregister_family as symbolic
Defining function register_pernet_subsys as symbolic
Defining function register_pernet_device as symbolic
Defining function nf_register_hooks as symbolic
Defining function nf_register_sockopt as symbolic
Defining function genl_register_family_with_ops as symbolic
Defining function strcat as symbolic
Defining function register_netdevice_notifier as symbolic
Removed calls to 'nf_ct_expect_init' (function is undefined)
Removed calls to 'nf_ct_expect_put' (function is undefined)
Defining function nf_ct_expect_alloc as symbolic
Defining function nf_ct_expect_related_report as symbolic
Linked our definitions to these undefined functions:
  strcmp
  strlen
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 1.88250184059
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 842 599 4609 32916
INFO: Starting verification
WARNING: this target does not support the llvm.returnaddress intrinsic.
WARNING: this target does not support the llvm.returnaddress intrinsic.
WARNING: this target does not support the llvm.returnaddress intrinsic.
KLEE: WARNING ONCE: function "tcp_conn_schedule" has inline asm
KLEE: WARNING ONCE: function "tcp_snat_handler" has inline asm
KLEE: WARNING ONCE: function "tcp_dnat_handler" has inline asm
KLEE: WARNING ONCE: function "tcp_csum_check" has inline asm
KLEE: WARNING ONCE: function "tcp_state_transition" has inline asm
KLEE: WARNING ONCE: function "tcp_register_app" has inline asm
KLEE: WARNING ONCE: function "tcp_unregister_app" has inline asm
KLEE: WARNING ONCE: function "udp_conn_schedule" has inline asm
KLEE: WARNING ONCE: function "udp_snat_handler" has inline asm
KLEE: WARNING ONCE: function "udp_dnat_handler" has inline asm
KLEE: WARNING ONCE: function "udp_csum_check" has inline asm
KLEE: WARNING ONCE: function "udp_register_app" has inline asm
KLEE: WARNING ONCE: function "udp_unregister_app" has inline asm
KLEE: WARNING ONCE: function "ip_vs_app_inc_get" has inline asm
KLEE: WARNING ONCE: function "ip_vs_dbg_addr___3" has inline asm
KLEE: WARNING ONCE: function "udp_partial_csum_update" has inline asm
KLEE: WARNING ONCE: function "udp_fast_csum_update" has inline asm
KLEE: WARNING ONCE: function "ip_vs_service_get" has inline asm
KLEE: WARNING ONCE: function "ip_vs_schedule" has inline asm
KLEE: WARNING ONCE: function "ip_vs_leave" has inline asm
KLEE: WARNING ONCE: function "skb_net___0" has inline asm
KLEE: WARNING ONCE: function "ip_vs_conn_new" has inline asm
KLEE: WARNING ONCE: function "ip_vs_in_stats" has inline asm
KLEE: WARNING ONCE: function "ip_vs_conn_put" has inline asm
KLEE: WARNING ONCE: function "ip_vs_conn_expire" has inline asm
KLEE: WARNING ONCE: function "ip_vs_bind_dest" has inline asm
KLEE: WARNING ONCE: function "ip_vs_tunnel_xmit" has inline asm
KLEE: WARNING ONCE: function "ip_vs_conn_hash" has inline asm
KLEE: WARNING ONCE: function "__ip_vs_get_out_rt" has inline asm
KLEE: WARNING ONCE: function "ip_vs_notrack" has inline asm
KLEE: WARNING ONCE: function "nf_conntrack_put" has inline asm
KLEE: WARNING ONCE: function "__ip_vs_dst_check" has inline asm
KLEE: WARNING ONCE: function "nf_reset" has inline asm
KLEE: WARNING ONCE: function "ip_vs_conn_fill_cport" has inline asm
KLEE: WARNING ONCE: function "__ip_vs_reroute_locally" has inline asm
KLEE: WARNING ONCE: function "ip_vs_conn_unhash" has inline asm
KLEE: WARNING ONCE: function "__ip_vs_get_out_rt_v6" has inline asm
KLEE: WARNING ONCE: function "ip_vs_dbg_addr" has inline asm
KLEE: WARNING ONCE: function "ip_vs_unbind_app" has inline asm
KLEE: WARNING ONCE: function "ip_vs_sync_conn" has inline asm
KLEE: WARNING ONCE: function "ip_vs_sync_conn_needed" has inline asm
KLEE: WARNING ONCE: function "ip_vs_dbg_addr___0" has inline asm
KLEE: WARNING ONCE: function "ip_vs_ct_in_get" has inline asm
KLEE: WARNING ONCE: function "ip_vs_check_template" has inline asm
KLEE: WARNING ONCE: function "ip_vs_dbg_addr___1" has inline asm
KLEE: WARNING ONCE: function "skb_net___4" has inline asm
KLEE: WARNING ONCE: function "ip_vs_conn_out_get" has inline asm
KLEE: WARNING ONCE: function "ip_vs_dbg_addr___4" has inline asm
KLEE: WARNING ONCE: function "__ip_vs_conn_in_get" has inline asm
KLEE: WARNING ONCE: function "sctp_conn_schedule" has inline asm
KLEE: WARNING ONCE: function "sctp_state_transition" has inline asm
KLEE: WARNING ONCE: function "sctp_register_app" has inline asm
KLEE: WARNING ONCE: function "sctp_unregister_app" has inline asm
KLEE: WARNING ONCE: function "ip_vs_dbg_addr___5" has inline asm
KLEE: WARNING ONCE: function "__ip_vs_init" has inline asm
KLEE: WARNING ONCE: function "__ip_vs_unbind_svc" has inline asm
KLEE: WARNING ONCE: function "ip_vs_unlink_service" has inline asm
KLEE: WARNING ONCE: function "__ip_vs_del_dest" 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 "estimation_timer" has inline asm
KLEE: WARNING ONCE: function "stop_sync_thread" has inline asm
KLEE: WARNING ONCE: function "ip_vs_in_icmp_v6" has inline asm
KLEE: WARNING ONCE: function "ip_vs_icmp_xmit_v6" has inline asm
KLEE: WARNING ONCE: function "ip_vs_in" has inline asm
KLEE: WARNING ONCE: function "ip_vs_in_icmp" has inline asm
KLEE: WARNING ONCE: function "__skb_pull" has inline asm
KLEE: WARNING ONCE: function "ip_vs_out_stats" has inline asm
KLEE: WARNING ONCE: function "ip_vs_icmp_xmit" has inline asm
KLEE: WARNING ONCE: function "ip_vs_nat_icmp" has inline asm
KLEE: WARNING ONCE: function "handle_response_icmp" has inline asm
KLEE: WARNING ONCE: function "ip_vs_stats_percpu_show" has inline asm
KLEE: WARNING ONCE: function "proc_do_defense_mode" has inline asm
KLEE: WARNING ONCE: function "do_ip_vs_get_ctl" has inline asm
KLEE: WARNING ONCE: function "start_sync_thread" has inline asm
KLEE: WARNING ONCE: function "ip_vs_add_service" has inline asm
KLEE: WARNING ONCE: function "ip_vs_edit_service" has inline asm
KLEE: WARNING ONCE: function "ip_vs_del_dest" has inline asm
KLEE: WARNING ONCE: function "__ip_vs_update_dest" has inline asm
KLEE: WARNING ONCE: function "sync_thread_master" has inline asm
KLEE: WARNING ONCE: function "sync_thread_backup" has inline asm
KLEE: WARNING ONCE: function "sk_change_net" has inline asm
KLEE: WARNING ONCE: function "ip_vs_proc_conn" has inline asm
KLEE: WARNING ONCE: function "ip_vs_find_dest" has inline asm
KLEE: WARNING ONCE: function "sb_dequeue" has inline asm
KLEE: WARNING ONCE: function "get_curr_sync_buff" has inline asm
KLEE: WARNING ONCE: function "skb_sknet" has inline asm
KLEE: WARNING ONCE: function "ip_vs_dbg_addr___2" has inline asm
KLEE: WARNING ONCE: function "tcp_partial_csum_update" has inline asm
KLEE: WARNING ONCE: function "tcp_fast_csum_update" has inline asm
KLEE: WARNING ONCE: function "ip_vs_conn_fill_param_proto" has inline asm
KLEE: WARNING ONCE: function "ip_vs_app_inc_put" has inline asm
KLEE: WARNING ONCE: function "ip_vs_checksum_complete" has inline asm
KLEE: WARNING: undefined reference to function: delayed_work_timer_fn
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/symbiotic-rLhxBJ/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-net--netfilter--ipvs--ip_vs.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:9906: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: flushing 9576 bytes on read, may be slow and/or crash: MO297[9576] allocated at global:
KLEE: ERROR: /tmp/symbiotic-rLhxBJ/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-net--netfilter--ipvs--ip_vs.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:9906: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
