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-mutex__drivers-net-netconsole_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.: 225 221 1181 6458
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.32239985466
Removed calls to 'netpoll_send_udp' (function is undefined)
Removed calls to 'config_item_put' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Defining function config_item_get as symbolic
Removed calls to 'configfs_unregister_subsystem' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to 'netpoll_cleanup' (function is undefined)
Defining function unregister_netdevice_notifier as symbolic
Defining function unregister_console as symbolic
Removed calls to '__list_add' (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 '__mutex_init' (function is undefined)
Removed calls to 'config_group_init' (function is undefined)
Removed calls to 'register_console' (function is undefined)
Defining function strnlen as symbolic
Defining function strsep as symbolic
Defining function printk as symbolic
Defining function configfs_register_subsystem as symbolic
Defining function register_netdevice_notifier as symbolic
Defining function strlcpy as symbolic
Defining function netpoll_parse_options as symbolic
Defining function netpoll_setup as symbolic
Removed calls to 'config_item_init_type_name' (function is undefined)
Defining function snprintf as symbolic
Removed calls to 'netpoll_print_options' (function is undefined)
Defining function kstrtoint as symbolic
Defining function strnchr as symbolic
Defining function in6_pton as symbolic
Defining function in_aton as symbolic
Defining function kstrtou16 as symbolic
Defining function mac_pton as symbolic
Removed calls to '__netpoll_cleanup' (function is undefined)
Defining function external_allocated_data as symbolic
Removed calls to 'ldv_assert' (function is undefined)
Linked our definitions to these undefined functions:
  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.32296204567
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 264 223 663 4131
INFO: Starting verification
KLEE: WARNING ONCE: function "netconsole_netdev_event" has inline asm
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_07714fa5-b54e-484e-8f4d-0ae5ab2150c7/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: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 29887 states (over memory cap)
KLEE: WARNING: killing 25715 states (over memory cap)
KLEE: WARNING: killing 25808 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-qn2fXY/linux-3.14__complex_emg__linux-kernel-locking-mutex__drivers-net-netconsole_true-unreach-call.cil.c:6188: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 25905 states (over memory cap)
KLEE: WARNING: killing 24664 states (over memory cap)
KLEE: WARNING: killing 24962 states (over memory cap)
KLEE: WARNING: killing 24300 states (over memory cap)
KLEE: WARNING: killing 24981 states (over memory cap)
KLEE: WARNING: killing 24333 states (over memory cap)
KLEE: WARNING: killing 23885 states (over memory cap)
KLEE: WARNING: killing 24367 states (over memory cap)
KLEE: WARNING: killing 25228 states (over memory cap)
KLEE: WARNING: killing 25353 states (over memory cap)
KLEE: WARNING: killing 25833 states (over memory cap)
KLEE: WARNING: killing 26320 states (over memory cap)
KLEE: WARNING: killing 26802 states (over memory cap)
KLEE: WARNING: killing 27275 states (over memory cap)
KLEE: WARNING: killing 27383 states (over memory cap)
KLEE: WARNING: killing 27490 states (over memory cap)
KLEE: WARNING: killing 28162 states (over memory cap)
KLEE: WARNING: killing 28445 states (over memory cap)
KLEE: WARNING: killing 28552 states (over memory cap)
KLEE: WARNING: killing 28485 states (over memory cap)
KLEE: WARNING: killing 29707 states (over memory cap)
KLEE: WARNING: killing 29446 states (over memory cap)
KLEE: WARNING: killing 29197 states (over memory cap)
KLEE: WARNING: killing 28942 states (over memory cap)
KLEE: WARNING: killing 29789 states (over memory cap)
KLEE: WARNING: killing 28802 states (over memory cap)
KLEE: WARNING: killing 28210 states (over memory cap)
KLEE: WARNING: killing 28678 states (over memory cap)
KLEE: WARNING: killing 28082 states (over memory cap)
KLEE: WARNING: killing 28007 states (over memory cap)
KLEE: WARNING: killing 27765 states (over memory cap)
KLEE: WARNING: killing 27355 states (over memory cap)
KLEE: WARNING: killing 27288 states (over memory cap)
KLEE: WARNING: killing 27593 states (over memory cap)
KLEE: WARNING: killing 27883 states (over memory cap)
KLEE: WARNING: killing 28160 states (over memory cap)
KLEE: WARNING: killing 27050 states (over memory cap)
KLEE: WARNING: killing 28210 states (over memory cap)
KLEE: WARNING: killing 27787 states (over memory cap)
KLEE: WARNING: killing 26853 states (over memory cap)
KLEE: WARNING: killing 27135 states (over memory cap)
KLEE: WARNING: killing 27593 states (over memory cap)
KLEE: WARNING: killing 27543 states (over memory cap)
KLEE: WARNING: killing 27301 states (over memory cap)
KLEE: WARNING: killing 28115 states (over memory cap)
KLEE: WARNING: killing 27195 states (over memory cap)
KLEE: WARNING: killing 28159 states (over memory cap)
KLEE: WARNING: killing 27244 states (over memory cap)
KLEE: WARNING: killing 27869 states (over memory cap)
KLEE: WARNING: killing 27477 states (over memory cap)
KLEE: WARNING: killing 28434 states (over memory cap)
KLEE: WARNING: killing 27867 states (over memory cap)
KLEE: WARNING: killing 27459 states (over memory cap)
KLEE: WARNING: killing 27229 states (over memory cap)
KLEE: WARNING: killing 27174 states (over memory cap)
KLEE: WARNING: killing 27969 states (over memory cap)
KLEE: WARNING: killing 27747 states (over memory cap)
KLEE: WARNING: killing 27675 states (over memory cap)
KLEE: WARNING: killing 27790 states (over memory cap)
KLEE: WARNING: killing 27220 states (over memory cap)
KLEE: WARNING: killing 27507 states (over memory cap)
KLEE: WARNING: killing 27959 states (over memory cap)
KLEE: WARNING: killing 28081 states (over memory cap)
KLEE: WARNING: killing 27684 states (over memory cap)
KLEE: WARNING: killing 27466 states (over memory cap)
KLEE: WARNING: killing 28230 states (over memory cap)
KLEE: WARNING: killing 28350 states (over memory cap)
KLEE: WARNING: killing 27313 states (over memory cap)
KLEE: WARNING: killing 27574 states (over memory cap)
KLEE: WARNING: killing 27519 states (over memory cap)
KLEE: WARNING: killing 27472 states (over memory cap)
KLEE: WARNING: killing 27898 states (over memory cap)
KLEE: WARNING: killing 28015 states (over memory cap)
KLEE: WARNING: killing 27628 states (over memory cap)
KLEE: WARNING: killing 27734 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-qn2fXY/linux-3.14__complex_emg__linux-kernel-locking-mutex__drivers-net-netconsole_true-unreach-call.cil.c:6145: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_07714fa5-b54e-484e-8f4d-0ae5ab2150c7/symbiotic/lib/kernel/kfree.c:5: free of global
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 27362 states (over memory cap)
KLEE: WARNING: killing 27802 states (over memory cap)
KLEE: WARNING: killing 27417 states (over memory cap)
KLEE: WARNING: killing 27527 states (over memory cap)
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_07714fa5-b54e-484e-8f4d-0ae5ab2150c7/symbiotic/lib/kernel/kfree.c:5: free of global
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 27155 states (over memory cap)
KLEE: WARNING: killing 27589 states (over memory cap)
KLEE: WARNING: killing 27533 states (over memory cap)
KLEE: WARNING: killing 27487 states (over memory cap)
KLEE: WARNING: killing 27749 states (over memory cap)
KLEE: WARNING: killing 28180 states (over memory cap)
KLEE: WARNING: killing 27336 states (over memory cap)
KLEE: WARNING: killing 27912 states (over memory cap)
KLEE: WARNING: killing 26757 states (over memory cap)
KLEE: WARNING: killing 27819 states (over memory cap)
KLEE: WARNING: killing 27939 states (over memory cap)
KLEE: WARNING: killing 27884 states (over memory cap)
KLEE: WARNING: killing 28633 states (over memory cap)
KLEE: WARNING: killing 27633 states (over memory cap)
KLEE: WARNING: killing 27428 states (over memory cap)
KLEE: WARNING: killing 27845 states (over memory cap)
KLEE: WARNING: killing 27794 states (over memory cap)
KLEE: WARNING: killing 27589 states (over memory cap)
KLEE: WARNING: killing 27711 states (over memory cap)
KLEE: WARNING: killing 28273 states (over memory cap)
KLEE: WARNING: killing 27289 states (over memory cap)
KLEE: WARNING: killing 27717 states (over memory cap)
KLEE: WARNING: killing 27672 states (over memory cap)
KLEE: WARNING: killing 27158 states (over memory cap)
KLEE: WARNING: killing 27418 states (over memory cap)
KLEE: WARNING: killing 26892 states (over memory cap)
KLEE: WARNING: killing 15422 states (over memory cap)
