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--core--pktgen.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.: 367 225 2534 17585
Removed infinite loop in net_generic
Removed infinite loop in pktgen_thread_show
Removed infinite loop in pktgen_thread_worker
Removed infinite loop in get_page
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.736788988113
Defining function seq_lseek as symbolic
Defining function seq_read as symbolic
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function single_release as symbolic
Defining function PDE_DATA as symbolic
Defining function single_open as symbolic
Defining function seq_puts 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)
Defining function capable as symbolic
Removed calls to 'might_fault' (function is undefined)
Removed calls to '__copy_from_user_overflow' (function is undefined)
Defining function printk as symbolic
Defining function msecs_to_jiffies as symbolic
Defining function schedule_timeout_interruptible as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function msleep_interruptible as symbolic
Defining function _copy_from_user as symbolic
Defining function debug_lockdep_rcu_enabled 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
Defining function seq_printf as symbolic
Defining function sprintf as symbolic
Defining function __cpu_to_node as symbolic
Defining function proc_create_data as symbolic
Defining function vzalloc_node as symbolic
Removed calls to 'proc_remove' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'remove_proc_entry' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Defining function kthread_stop as symbolic
Defining function proc_mkdir as symbolic
Defining function find_next_bit as symbolic
Defining function ktime_get as symbolic
Defining function ns_to_timeval as symbolic
Defining function in_aton as symbolic
Defining function pskb_expand_head as symbolic
Defining function __netdev_alloc_skb as symbolic
Removed calls to 'put_page' (function is undefined)
Defining function in6_pton as symbolic
Defining function snprintf as symbolic
Defining function mac_pton as symbolic
Defining function hex_to_bin as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'unregister_pernet_subsys' (function is undefined)
Removed calls to 'ldv_check_final_state' (function is undefined)
Defining function register_pernet_subsys as symbolic
Defining function register_netdevice_notifier as symbolic
Defining function unregister_netdevice_notifier as symbolic
Defining function kmem_cache_alloc as symbolic
Defining function skb_clone as symbolic
Defining function skb_copy as symbolic
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  strcmp
  strcpy
  strlen
  strncmp
  strncpy
  __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_ulong_named
INFO: After-slicing optimizations and preparation time: 0.529749155045
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 410 110 1176 5955
INFO: Starting verification
KLEE: WARNING ONCE: function "pgctrl_write" has inline asm
KLEE: WARNING ONCE: function "net_generic" has inline asm
KLEE: WARNING ONCE: function "pktgen_wait_all_threads_run" has inline asm
KLEE: WARNING ONCE: function "pktgen_if_write" has inline asm
KLEE: WARNING ONCE: function "count_trail_chars" has inline asm
KLEE: WARNING ONCE: function "strn_len" has inline asm
KLEE: WARNING ONCE: function "num_arg" has inline asm
KLEE: WARNING ONCE: function "hex32_arg" has inline asm
KLEE: WARNING ONCE: function "pktgen_thread_show" has inline asm
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_6f9e50aa-3831-4c00-88ce-c5c31ba94406/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 5598 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 6131 states (over memory cap)
KLEE: WARNING: killing 6664 states (over memory cap)
KLEE: WARNING: killing 6980 states (over memory cap)
KLEE: WARNING: killing 7351 states (over memory cap)
KLEE: WARNING: killing 8314 states (over memory cap)
KLEE: WARNING: killing 8576 states (over memory cap)
KLEE: WARNING: killing 8728 states (over memory cap)
KLEE: WARNING: killing 9096 states (over memory cap)
KLEE: WARNING: killing 9086 states (over memory cap)
KLEE: WARNING: killing 9129 states (over memory cap)
KLEE: WARNING: killing 9063 states (over memory cap)
KLEE: WARNING: killing 9049 states (over memory cap)
KLEE: WARNING: killing 9087 states (over memory cap)
KLEE: WARNING: killing 9289 states (over memory cap)
KLEE: WARNING: killing 9917 states (over memory cap)
KLEE: WARNING: killing 9581 states (over memory cap)
KLEE: WARNING: killing 10049 states (over memory cap)
KLEE: WARNING: killing 10352 states (over memory cap)
KLEE: WARNING: killing 10286 states (over memory cap)
KLEE: WARNING: killing 9796 states (over memory cap)
KLEE: WARNING: killing 10101 states (over memory cap)
KLEE: WARNING: killing 10930 states (over memory cap)
KLEE: WARNING: killing 9913 states (over memory cap)
KLEE: WARNING: killing 10427 states (over memory cap)
KLEE: WARNING: killing 10303 states (over memory cap)
KLEE: WARNING: killing 10237 states (over memory cap)
KLEE: WARNING: killing 10274 states (over memory cap)
KLEE: WARNING: killing 10000 states (over memory cap)
KLEE: WARNING: killing 9932 states (over memory cap)
KLEE: WARNING: killing 10283 states (over memory cap)
KLEE: WARNING: killing 10530 states (over memory cap)
KLEE: WARNING: killing 10361 states (over memory cap)
KLEE: WARNING: killing 10195 states (over memory cap)
KLEE: WARNING: killing 10547 states (over memory cap)
KLEE: WARNING: killing 10219 states (over memory cap)
KLEE: WARNING: killing 10048 states (over memory cap)
KLEE: WARNING: killing 10195 states (over memory cap)
KLEE: WARNING: killing 10233 states (over memory cap)
KLEE: WARNING: killing 10429 states (over memory cap)
KLEE: WARNING: killing 9948 states (over memory cap)
KLEE: WARNING: killing 10506 states (over memory cap)
KLEE: WARNING: killing 10390 states (over memory cap)
KLEE: WARNING: killing 10022 states (over memory cap)
KLEE: WARNING: killing 9905 states (over memory cap)
KLEE: WARNING: killing 10251 states (over memory cap)
KLEE: WARNING: killing 10140 states (over memory cap)
KLEE: WARNING: killing 10280 states (over memory cap)
KLEE: WARNING: killing 10066 states (over memory cap)
KLEE: WARNING: killing 10154 states (over memory cap)
KLEE: WARNING: killing 10096 states (over memory cap)
KLEE: WARNING: killing 10234 states (over memory cap)
KLEE: WARNING: killing 10068 states (over memory cap)
KLEE: WARNING: killing 10313 states (over memory cap)
KLEE: WARNING: killing 10659 states (over memory cap)
KLEE: WARNING: killing 10496 states (over memory cap)
KLEE: WARNING: killing 10028 states (over memory cap)
KLEE: WARNING: killing 10217 states (over memory cap)
KLEE: WARNING: killing 10053 states (over memory cap)
KLEE: WARNING: killing 10042 states (over memory cap)
KLEE: WARNING: killing 9983 states (over memory cap)
KLEE: WARNING: killing 10072 states (over memory cap)
KLEE: WARNING: killing 9855 states (over memory cap)
KLEE: WARNING: killing 10046 states (over memory cap)
KLEE: WARNING: killing 10441 states (over memory cap)
KLEE: WARNING: killing 10431 states (over memory cap)
KLEE: WARNING: killing 10271 states (over memory cap)
KLEE: WARNING: killing 9759 states (over memory cap)
KLEE: WARNING: killing 10402 states (over memory cap)
KLEE: WARNING: killing 10340 states (over memory cap)
KLEE: WARNING: killing 10385 states (over memory cap)
KLEE: WARNING: killing 10273 states (over memory cap)
KLEE: WARNING: killing 9815 states (over memory cap)
KLEE: WARNING: killing 9951 states (over memory cap)
KLEE: WARNING: killing 10394 states (over memory cap)
KLEE: WARNING: killing 9881 states (over memory cap)
KLEE: WARNING: killing 10074 states (over memory cap)
KLEE: WARNING: killing 9662 states (over memory cap)
KLEE: WARNING: killing 10250 states (over memory cap)
KLEE: WARNING: killing 10140 states (over memory cap)
KLEE: WARNING: killing 10033 states (over memory cap)
KLEE: WARNING: killing 10121 states (over memory cap)
KLEE: WARNING: killing 10213 states (over memory cap)
KLEE: WARNING: killing 10201 states (over memory cap)
KLEE: WARNING: killing 10289 states (over memory cap)
KLEE: WARNING: killing 10577 states (over memory cap)
KLEE: WARNING: killing 10173 states (over memory cap)
KLEE: WARNING: killing 9817 states (over memory cap)
KLEE: WARNING: killing 10152 states (over memory cap)
KLEE: WARNING: killing 10190 states (over memory cap)
KLEE: WARNING: killing 10627 states (over memory cap)
KLEE: WARNING: killing 10222 states (over memory cap)
KLEE: WARNING: killing 9822 states (over memory cap)
KLEE: WARNING: killing 10104 states (over memory cap)
KLEE: WARNING: killing 10288 states (over memory cap)
KLEE: WARNING: killing 10134 states (over memory cap)
KLEE: WARNING: killing 10568 states (over memory cap)
KLEE: WARNING: killing 10310 states (over memory cap)
KLEE: WARNING: killing 10400 states (over memory cap)
KLEE: WARNING: killing 10685 states (over memory cap)
KLEE: WARNING: killing 10134 states (over memory cap)
KLEE: WARNING: killing 9687 states (over memory cap)
KLEE: WARNING: killing 10362 states (over memory cap)
KLEE: WARNING: killing 9667 states (over memory cap)
KLEE: WARNING: killing 10530 states (over memory cap)
KLEE: WARNING: killing 10032 states (over memory cap)
KLEE: WARNING: killing 10270 states (over memory cap)
KLEE: WARNING: killing 10162 states (over memory cap)
KLEE: WARNING: killing 10396 states (over memory cap)
KLEE: WARNING: killing 10148 states (over memory cap)
KLEE: WARNING: killing 10429 states (over memory cap)
KLEE: WARNING: killing 10226 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-4dPwb6/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-net--core--pktgen.ko-entry_point_true-unreach-call.cil.out.c:7066: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 10263 states (over memory cap)
KLEE: WARNING: killing 10591 states (over memory cap)
KLEE: WARNING: killing 9956 states (over memory cap)
KLEE: WARNING: killing 9897 states (over memory cap)
KLEE: WARNING: killing 10034 states (over memory cap)
KLEE: WARNING: killing 10215 states (over memory cap)
KLEE: WARNING: killing 10255 states (over memory cap)
KLEE: WARNING: killing 10242 states (over memory cap)
KLEE: WARNING: killing 10667 states (over memory cap)
KLEE: WARNING: killing 10129 states (over memory cap)
KLEE: WARNING: killing 10457 states (over memory cap)
KLEE: WARNING: killing 10545 states (over memory cap)
KLEE: WARNING: killing 10156 states (over memory cap)
KLEE: WARNING: killing 9907 states (over memory cap)
KLEE: WARNING: killing 10091 states (over memory cap)
KLEE: WARNING: killing 10131 states (over memory cap)
KLEE: WARNING: killing 10210 states (over memory cap)
KLEE: WARNING: killing 10204 states (over memory cap)
KLEE: WARNING: killing 10148 states (over memory cap)
KLEE: WARNING: killing 10141 states (over memory cap)
KLEE: WARNING: killing 10323 states (over memory cap)
KLEE: WARNING: killing 9979 states (over memory cap)
KLEE: WARNING: killing 10065 states (over memory cap)
KLEE: WARNING: killing 10531 states (over memory cap)
KLEE: WARNING: killing 10141 states (over memory cap)
KLEE: WARNING: killing 10277 states (over memory cap)
KLEE: WARNING: killing 10504 states (over memory cap)
KLEE: WARNING: killing 10544 states (over memory cap)
KLEE: WARNING: killing 10155 states (over memory cap)
KLEE: WARNING: killing 9909 states (over memory cap)
KLEE: WARNING: killing 10377 states (over memory cap)
KLEE: WARNING: killing 9847 states (over memory cap)
