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_consumption_linux-3.16-rc1.tar.xz-43_2a-net--batman-adv--batman-adv.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.: 601 1075 11401 75587
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 2.80388402939
Removed calls to 'dump_stack' (function is undefined)
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to 'sysfs_remove_file_ns' (function is undefined)
Removed calls to 'kobject_put' (function is undefined)
Removed calls to 'lockdep_rcu_suspicious' (function is undefined)
Removed calls to 'call_rcu_sched' (function is undefined)
Defining function crc16 as symbolic
Removed calls to '_raw_spin_unlock_bh' (function is undefined)
Removed calls to '_raw_spin_lock_bh' (function is undefined)
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
Removed calls to '__dev_kfree_skb_any' (function is undefined)
Defining function arp_create as symbolic
Removed calls to 'ldv__builtin_va_start' (function is undefined)
Removed calls to 'ldv__builtin_va_end' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Defining function eth_type_trans as symbolic
Defining function netif_rx as symbolic
Defining function skb_push as symbolic
Defining function pskb_expand_head as symbolic
Defining function vscnprintf as symbolic
Defining function jiffies_to_msecs as symbolic
Defining function rcu_lockdep_current_cpu_online as symbolic
Defining function lock_is_held as symbolic
Removed calls to 'kfree_call_rcu' (function is undefined)
Defining function msecs_to_jiffies as symbolic
Defining function printk as symbolic
Defining function net_ratelimit as symbolic
Defining function crc32c as symbolic
Defining function dev_get_by_index as symbolic
Removed calls to 'kfree_skb' (function is undefined)
Defining function skb_put as symbolic
Removed calls to 'skb_split' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to 'get_random_bytes' (function is undefined)
Defining function dev_queue_xmit as symbolic
Defining function skb_pull_rcsum as symbolic
Removed calls to 'skb_prepare_seq_read' (function is undefined)
Defining function skb_seq_read as symbolic
Defining function __pskb_pull_tail as symbolic
Defining function skb_clone as symbolic
Defining function __pskb_copy_fclone as symbolic
Defining function __netdev_alloc_skb as symbolic
Defining function netdev_master_upper_dev_get_rcu as symbolic
Defining function rtnl_is_locked as symbolic
Removed calls to 'dev_remove_pack' (function is undefined)
Removed calls to 'netdev_upper_dev_unlink' (function is undefined)
Defining function queue_work_on as symbolic
Defining function sprintf as symbolic
Defining function cancel_delayed_work_sync as symbolic
Removed calls to 'debugfs_remove_recursive' (function is undefined)
Defining function debugfs_create_dir as symbolic
Defining function debugfs_create_file as symbolic
Defining function kobject_create_and_add as symbolic
Defining function sysfs_create_file_ns as symbolic
Defining function __dev_get_by_index as symbolic
Defining function kobject_get as symbolic
Defining function queue_delayed_work_on as symbolic
Defining function skb_copy as symbolic
Defining function skb_copy_bits as symbolic
Removed calls to 'ether_setup' (function is undefined)
Removed calls to 'unregister_netdevice_queue' (function is undefined)
Removed calls to 'rcu_barrier' (function is undefined)
Removed calls to 'free_netdev' (function is undefined)
Removed calls to 'free_percpu' (function is undefined)
Removed calls to '__bitmap_shift_left' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function seq_printf as symbolic
Defining function seq_puts as symbolic
Defining function prandom_u32 as symbolic
Defining function __bitmap_weight as symbolic
Defining function seq_lseek as symbolic
Defining function seq_read as symbolic
Defining function single_release as symbolic
Defining function single_open as symbolic
Defining function no_llseek as symbolic
Defining function try_module_get as symbolic
Defining function nonseekable_open as symbolic
Defining function prepare_to_wait_event as symbolic
Removed calls to 'finish_wait' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'might_fault' (function is undefined)
Removed calls to '__copy_to_user_overflow' (function is undefined)
Removed calls to '__copy_from_user_overflow' (function is undefined)
Removed calls to 'module_put' (function is undefined)
Defining function _copy_from_user as symbolic
Defining function _copy_to_user as symbolic
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to '__init_work' (function is undefined)
Defining function eth_validate_addr as symbolic
Removed calls to 'dev_add_pack' (function is undefined)
Defining function dev_get_by_name as symbolic
Defining function netdev_master_upper_dev_get as symbolic
Defining function netdev_master_upper_dev_link as symbolic
Removed calls to 'consume_skb' (function is undefined)
Defining function alloc_netdev_mqs as symbolic
Defining function register_netdevice as symbolic
Defining function find_next_bit as symbolic
Removed calls to 'unregister_netdev' (function is undefined)
Defining function __alloc_percpu as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'init_timer_key' (function is undefined)
Defining function debugfs_create_u8 as symbolic
Defining function debugfs_create_u32 as symbolic
Defining function strlcpy as symbolic
Defining function kstrtoull as symbolic
Defining function strnicmp as symbolic
Defining function kstrtoll as symbolic
Defining function kstrtouint as symbolic
Removed calls to 'rtnl_lock' (function is undefined)
Removed calls to 'rtnl_unlock' (function is undefined)
Defining function kmem_cache_alloc as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'rtnl_link_unregister' (function is undefined)
Removed calls to 'flush_workqueue' (function is undefined)
Removed calls to 'destroy_workqueue' (function is undefined)
Removed calls to 'ldv_check_final_state' (function is undefined)
Defining function param_get_string as symbolic
Defining function ldv_release_19 as symbolic
Defining function ldv_init_19 as symbolic
Defining function __alloc_workqueue_key as symbolic
Defining function register_netdevice_notifier as symbolic
Defining function rtnl_link_register as symbolic
Removed calls to 'nf_conntrack_destroy' (function is undefined)
Defining function ___pskb_trim as symbolic
Defining function unregister_netdevice_notifier as symbolic
Defining function param_set_copystring as symbolic
Defining function ldv_ndo_uninit_20 as symbolic
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  memcmp
  strchr
  strcmp
  strlen
  strncmp
  __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_u32_named
  __VERIFIER_nondet_ulong_named
INFO: After-slicing optimizations and preparation time: 2.76067900658
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 813 768 6207 39620
INFO: Starting verification
KLEE: WARNING ONCE: function "batadv_hard_if_event" has inline asm
KLEE: WARNING ONCE: function "batadv_interface_tx" has inline asm
KLEE: WARNING ONCE: function "batadv_hardif_get_by_netdev" 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 "batadv_primary_if_get_selected" has inline asm
KLEE: WARNING ONCE: function "batadv_hardif_free_ref" has inline asm
KLEE: WARNING ONCE: function "batadv_bla_purge_backbone_gw" has inline asm
KLEE: WARNING ONCE: function "batadv_bla_send_claim" has inline asm
KLEE: WARNING ONCE: function "batadv_backbone_gw_free_ref" has inline asm
KLEE: WARNING ONCE: function "batadv_claim_free_ref" has inline asm
KLEE: WARNING ONCE: function "batadv_backbone_hash_find" has inline asm
KLEE: WARNING ONCE: function "batadv_claim_hash_find" has inline asm
KLEE: WARNING ONCE: function "batadv_tt_local_commit_changes_nolock" has inline asm
KLEE: WARNING ONCE: function "batadv_tt_local_size_mod" has inline asm
KLEE: WARNING ONCE: function "batadv_softif_vlan_get" has inline asm
KLEE: WARNING ONCE: function "batadv_softif_vlan_free_ref" has inline asm
KLEE: WARNING ONCE: function "batadv_tvlv_container_unregister" has inline asm
KLEE: WARNING ONCE: function "batadv_tt_local_add" has inline asm
KLEE: WARNING ONCE: function "batadv_tt_hash_find" has inline asm
KLEE: WARNING ONCE: function "batadv_tvlv_unicast_send" has inline asm
KLEE: WARNING ONCE: function "batadv_tt_local_entry_free_ref" has inline asm
KLEE: WARNING ONCE: function "batadv_tt_global_entry_free_ref" has inline asm
KLEE: WARNING ONCE: function "batadv_tt_global_del_orig_entry" has inline asm
KLEE: WARNING ONCE: function "batadv_orig_node_vlan_free_ref" has inline asm
KLEE: WARNING ONCE: function "batadv_tt_orig_list_entry_free_ref" has inline asm
KLEE: WARNING ONCE: function "batadv_orig_node_vlan_get" has inline asm
KLEE: WARNING ONCE: function "batadv_orig_node_free_ref" has inline asm
KLEE: WARNING ONCE: function "batadv_find_router" has inline asm
KLEE: WARNING ONCE: function "batadv_frag_send_packet" has inline asm
KLEE: WARNING ONCE: function "batadv_nc_skb_forward" has inline asm
KLEE: WARNING ONCE: function "batadv_neigh_node_free_ref" has inline asm
KLEE: WARNING ONCE: function "batadv_nc_get_path" has inline asm
KLEE: WARNING ONCE: function "batadv_nc_path_free_ref" has inline asm
KLEE: WARNING ONCE: function "batadv_orig_router_get" has inline asm
KLEE: WARNING ONCE: function "batadv_neigh_ifinfo_get" has inline asm
KLEE: WARNING ONCE: function "batadv_neigh_ifinfo_free_ref" has inline asm
KLEE: WARNING ONCE: function "batadv_orig_ifinfo_free_ref" has inline asm
KLEE: WARNING ONCE: function "batadv_tvlv_container_free_ref" has inline asm
KLEE: WARNING ONCE: function "batadv_hardif_disable_interface" has inline asm
KLEE: WARNING ONCE: function "batadv_primary_if_select" has inline asm
KLEE: WARNING ONCE: function "batadv_gw_get_selected_gw_node" has inline asm
KLEE: WARNING ONCE: function "batadv_gw_select" has inline asm
KLEE: WARNING ONCE: function "batadv_gw_node_free_ref" has inline asm
KLEE: WARNING ONCE: function "batadv_gw_node_update" has inline asm
KLEE: WARNING ONCE: function "batadv_find_best_neighbor" has inline asm
KLEE: WARNING ONCE: function "batadv_update_route" has inline asm
KLEE: WARNING ONCE: function "batadv_gw_election" has inline asm
KLEE: WARNING ONCE: function "batadv_orig_ifinfo_get" has inline asm
KLEE: WARNING ONCE: function "batadv_gw_node_get" has inline asm
KLEE: WARNING ONCE: function "batadv_bla_tx" has inline asm
KLEE: WARNING ONCE: function "batadv_mcast_forw_mode" has inline asm
KLEE: WARNING ONCE: function "batadv_add_bcast_packet_to_list" has inline asm
KLEE: WARNING ONCE: function "batadv_gw_get_selected_orig" has inline asm
KLEE: WARNING ONCE: function "batadv_transtable_search" has inline asm
KLEE: WARNING ONCE: function "batadv_dat_entry_hash_find" has inline asm
KLEE: WARNING ONCE: function "batadv_dat_entry_free_ref" has inline asm
KLEE: WARNING ONCE: function "batadv_handle_claim" has inline asm
KLEE: WARNING ONCE: function "batadv_tvlv_handler_get" has inline asm
KLEE: WARNING ONCE: function "batadv_tvlv_handler_free_ref" has inline asm
KLEE: WARNING ONCE: function "batadv_iv_ogm_schedule" has inline asm
KLEE: WARNING ONCE: function "batadv_iv_ogm_emit" has inline asm
KLEE: WARNING ONCE: function "batadv_iv_ogm_queue_add" has inline asm
KLEE: WARNING ONCE: function "batadv_socket_read" has inline asm
KLEE: WARNING ONCE: function "batadv_socket_write" has inline asm
KLEE: WARNING ONCE: function "batadv_interface_open" has inline asm
KLEE: WARNING ONCE: function "batadv_interface_release" has inline asm
KLEE: WARNING ONCE: function "batadv_hardif_enable_interface" has inline asm
KLEE: WARNING ONCE: function "batadv_sum_counter" has inline asm
KLEE: WARNING ONCE: function "batadv_kobj_to_vlan" has inline asm
KLEE: WARNING ONCE: function "batadv_hardif_free_rcu" has inline asm
KLEE: WARNING ONCE: function "batadv_orig_node_free_ref_now" has inline asm
KLEE: WARNING ONCE: function "batadv_orig_node_free_rcu" has inline asm
KLEE: WARNING ONCE: function "batadv_neigh_node_free_ref_now" has inline asm
KLEE: WARNING ONCE: function "batadv_mcast_purge_orig" has inline asm
KLEE: WARNING ONCE: function "batadv_nc_node_free_ref" has inline asm
KLEE: WARNING ONCE: function "batadv_mcast_want_unsnoop_update" has inline asm
KLEE: WARNING ONCE: function "batadv_mcast_want_ipv4_update" has inline asm
KLEE: WARNING ONCE: function "batadv_mcast_want_ipv6_update" has inline asm
KLEE: WARNING ONCE: function "batadv_hardif_free_ref_now" has inline asm
KLEE: WARNING ONCE: function "batadv_neigh_node_free_rcu" has inline asm
KLEE: WARNING ONCE: function "batadv_send_outstanding_bat_ogm_packet" has inline asm
KLEE: WARNING ONCE: function "batadv_bit_get_packet" has inline asm
KLEE: WARNING ONCE: function "batadv_iv_ogm_receive" has inline asm
KLEE: WARNING ONCE: function "batadv_route_unicast_packet" has inline asm
KLEE: WARNING ONCE: function "batadv_orig_hash_find___5" has inline asm
KLEE: WARNING ONCE: function "batadv_iv_ogm_orig_get" has inline asm
KLEE: WARNING ONCE: function "batadv_iv_ogm_process_per_outif" has inline asm
KLEE: WARNING ONCE: function "batadv_nc_get_nc_node" has inline asm
KLEE: WARNING ONCE: function "batadv_neigh_node_get" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_35" has inline asm
KLEE: WARNING ONCE: function "batadv_dat_snoop_incoming_arp_request" has inline asm
KLEE: WARNING ONCE: function "batadv_frag_skb_fwd" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_20" has inline asm
KLEE: WARNING ONCE: function "batadv_recv_bcast_packet" has inline asm
KLEE: WARNING ONCE: function "batadv_recv_unicast_packet" has inline asm
KLEE: WARNING ONCE: function "batadv_recv_frag_packet" has inline asm
KLEE: WARNING ONCE: function "batadv_nc_recv_coded_packet" has inline asm
KLEE: WARNING ONCE: function "batadv_interface_rx" has inline asm
KLEE: WARNING ONCE: function "batadv_tt_global_orig_entry_find" has inline asm
KLEE: WARNING: undefined reference to function: __VERIFIER_nondet_u16_named
KLEE: WARNING: undefined reference to function: delayed_work_timer_fn
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_12f5c860-2475-46e0-a0c5-56fddec62b86/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16640 states (over memory cap)
KLEE: WARNING: killing 36678 states (over memory cap)
KLEE: WARNING: killing 33700 states (over memory cap)
KLEE: WARNING: killing 33355 states (over memory cap)
KLEE: WARNING: killing 33064 states (over memory cap)
KLEE: WARNING: killing 33205 states (over memory cap)
KLEE: WARNING: killing 30495 states (over memory cap)
KLEE: WARNING: killing 36315 states (over memory cap)
KLEE: WARNING: killing 36978 states (over memory cap)
KLEE: WARNING: killing 38285 states (over memory cap)
KLEE: WARNING: killing 41530 states (over memory cap)
KLEE: WARNING: killing 41557 states (over memory cap)
KLEE: WARNING: killing 36819 states (over memory cap)
KLEE: WARNING: killing 36533 states (over memory cap)
KLEE: WARNING: killing 33454 states (over memory cap)
KLEE: WARNING: killing 37640 states (over memory cap)
KLEE: WARNING: killing 35332 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 37451 states (over memory cap)
KLEE: WARNING: killing 38365 states (over memory cap)
KLEE: WARNING: killing 36316 states (over memory cap)
KLEE: WARNING: killing 36676 states (over memory cap)
KLEE: WARNING: killing 36038 states (over memory cap)
KLEE: WARNING: killing 35055 states (over memory cap)
KLEE: WARNING: killing 38950 states (over memory cap)
KLEE: WARNING: killing 36307 states (over memory cap)
KLEE: WARNING: killing 37070 states (over memory cap)
KLEE: WARNING: killing 36824 states (over memory cap)
KLEE: WARNING: killing 37872 states (over memory cap)
KLEE: WARNING: killing 37734 states (over memory cap)
KLEE: WARNING: killing 36010 states (over memory cap)
KLEE: WARNING: killing 37954 states (over memory cap)
KLEE: WARNING: killing 37570 states (over memory cap)
KLEE: WARNING: killing 33814 states (over memory cap)
KLEE: WARNING: killing 38608 states (over memory cap)
KLEE: WARNING: killing 37832 states (over memory cap)
KLEE: WARNING: killing 37688 states (over memory cap)
KLEE: WARNING: killing 36329 states (over memory cap)
KLEE: WARNING: killing 35939 states (over memory cap)
KLEE: WARNING: killing 37963 states (over memory cap)
KLEE: WARNING: killing 36557 states (over memory cap)
KLEE: WARNING: killing 36993 states (over memory cap)
KLEE: WARNING: killing 37796 states (over memory cap)
KLEE: WARNING: killing 37117 states (over memory cap)
KLEE: WARNING: killing 37909 states (over memory cap)
KLEE: WARNING: killing 36444 states (over memory cap)
KLEE: WARNING: killing 36794 states (over memory cap)
KLEE: WARNING: killing 38624 states (over memory cap)
KLEE: WARNING: killing 36247 states (over memory cap)
KLEE: WARNING: killing 36597 states (over memory cap)
KLEE: WARNING: killing 37333 states (over memory cap)
KLEE: WARNING: killing 38268 states (over memory cap)
KLEE: WARNING: killing 37065 states (over memory cap)
KLEE: WARNING: killing 36883 states (over memory cap)
KLEE: WARNING: killing 37082 states (over memory cap)
KLEE: WARNING: killing 36033 states (over memory cap)
KLEE: WARNING: killing 39212 states (over memory cap)
KLEE: WARNING: killing 36895 states (over memory cap)
KLEE: WARNING: killing 37830 states (over memory cap)
KLEE: WARNING: killing 35822 states (over memory cap)
KLEE: WARNING: killing 36272 states (over memory cap)
KLEE: WARNING: killing 37146 states (over memory cap)
KLEE: WARNING: killing 36678 states (over memory cap)
KLEE: WARNING: killing 37502 states (over memory cap)
KLEE: WARNING: killing 36131 states (over memory cap)
KLEE: WARNING: killing 36576 states (over memory cap)
KLEE: WARNING: killing 40528 states (over memory cap)
KLEE: WARNING: killing 36656 states (over memory cap)
KLEE: WARNING: killing 37196 states (over memory cap)
KLEE: WARNING: killing 35930 states (over memory cap)
KLEE: WARNING: killing 36084 states (over memory cap)
KLEE: WARNING: killing 37291 states (over memory cap)
KLEE: WARNING: killing 36967 states (over memory cap)
KLEE: WARNING: killing 35832 states (over memory cap)
KLEE: WARNING: killing 37090 states (over memory cap)
KLEE: WARNING: killing 38637 states (over memory cap)
KLEE: WARNING: killing 36860 states (over memory cap)
KLEE: WARNING: killing 37492 states (over memory cap)
KLEE: WARNING: killing 37272 states (over memory cap)
KLEE: WARNING: killing 37046 states (over memory cap)
KLEE: WARNING: killing 36598 states (over memory cap)
KLEE: WARNING: killing 35469 states (over memory cap)
KLEE: WARNING: killing 38797 states (over memory cap)
KLEE: WARNING: killing 36583 states (over memory cap)
KLEE: WARNING: killing 37835 states (over memory cap)
KLEE: WARNING: killing 36147 states (over memory cap)
KLEE: WARNING: killing 38490 states (over memory cap)
KLEE: WARNING: killing 36149 states (over memory cap)
