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/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ppp--ppp_synctty.ko-entry_point_false-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.: 34 98 528 3081
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.260612010956
Removed calls to 'might_fault' (function is undefined)
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Removed calls to '__copy_to_user_overflow' (function is undefined)
Defining function _copy_from_user as symbolic
Defining function _copy_to_user as symbolic
Removed calls to '_raw_spin_unlock_bh' (function is undefined)
Defining function skb_pull as symbolic
Defining function skb_put as symbolic
Defining function skb_push as symbolic
Defining function printk as symbolic
Defining function _raw_spin_trylock_bh as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'tasklet_init' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to '_raw_write_lock_irq' (function is undefined)
Removed calls to '_raw_write_unlock_irq' (function is undefined)
Removed calls to 'wait_for_completion' (function is undefined)
Removed calls to 'tasklet_kill' (function is undefined)
Removed calls to 'ppp_unregister_channel' (function is undefined)
Removed calls to 'skb_queue_purge' (function is undefined)
Removed calls to '_raw_spin_lock_bh' (function is undefined)
Removed calls to 'ppp_output_wakeup' (function is undefined)
Removed calls to 'skb_queue_tail' (function is undefined)
Removed calls to 'skb_trim' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'tty_unthrottle' (function is undefined)
Removed calls to '_raw_read_lock' (function is undefined)
Removed calls to '_raw_read_unlock' (function is undefined)
Removed calls to '__tasklet_schedule' (function is undefined)
Removed calls to 'complete' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Defining function ppp_channel_index as symbolic
Defining function ppp_unit_number as symbolic
Defining function n_tty_ioctl_helper as symbolic
Defining function tty_mode_ioctl as symbolic
Removed calls to 'ppp_input_error' (function is undefined)
Removed calls to 'ppp_input' (function is undefined)
Defining function ppp_register_channel as symbolic
Defining function tty_termios_baud_rate as symbolic
Defining function tty_register_ldisc as symbolic
Defining function tty_unregister_ldisc as symbolic
Linked our definitions to these undefined functions:
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_assume
  __VERIFIER_calloc0
  __VERIFIER_error
  __VERIFIER_exit
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
  __VERIFIER_nondet_pointer_named
  __VERIFIER_nondet_size_t_named
  __VERIFIER_nondet_uint_named
  __VERIFIER_nondet_ulong_named
INFO: After-slicing optimizations and preparation time: 0.275055885315
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 75 82 277 1693
INFO: Starting verification
KLEE: WARNING ONCE: function "ppp_sync_send" has inline asm
KLEE: WARNING ONCE: function "ppp_sync_ioctl" has inline asm
KLEE: WARNING ONCE: function "ppp_sync_push" has inline asm
KLEE: WARNING ONCE: function "ppp_sync_close" has inline asm
KLEE: WARNING ONCE: function "ppp_synctty_ioctl" has inline asm
KLEE: WARNING ONCE: function "ppp_sync_wakeup" has inline asm
KLEE: WARNING ONCE: function "sp_get" has inline asm
KLEE: WARNING ONCE: function "tasklet_schedule" has inline asm
KLEE: WARNING ONCE: function "sp_put" 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_a6846b15-06fb-4850-89cb-32098ad0d86f/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-kgC5Fl/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ppp--ppp_synctty.ko-entry_point_false-unreach-call.cil.out.c:6558: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-kgC5Fl/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ppp--ppp_synctty.ko-entry_point_false-unreach-call.cil.out.c:5844: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-kgC5Fl/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ppp--ppp_synctty.ko-entry_point_false-unreach-call.cil.out.c:5938: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-kgC5Fl/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ppp--ppp_synctty.ko-entry_point_false-unreach-call.cil.out.c:6235: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-kgC5Fl/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ppp--ppp_synctty.ko-entry_point_false-unreach-call.cil.out.c:6589: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 13023 states (over memory cap)
KLEE: WARNING: killing 13317 states (over memory cap)
KLEE: WARNING: killing 13044 states (over memory cap)
KLEE: WARNING: killing 13065 states (over memory cap)
KLEE: WARNING: killing 13287 states (over memory cap)
KLEE: WARNING: killing 13325 states (over memory cap)
KLEE: WARNING: killing 9369 states (over memory cap)
KLEE: WARNING: killing 12959 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-kgC5Fl/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ppp--ppp_synctty.ko-entry_point_false-unreach-call.cil.out.c:6403: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-kgC5Fl/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ppp--ppp_synctty.ko-entry_point_false-unreach-call.cil.out.c:6271: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-kgC5Fl/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ppp--ppp_synctty.ko-entry_point_false-unreach-call.cil.out.c:6287: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-kgC5Fl/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ppp--ppp_synctty.ko-entry_point_false-unreach-call.cil.out.c:6365: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-kgC5Fl/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ppp--ppp_synctty.ko-entry_point_false-unreach-call.cil.out.c:6436: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-kgC5Fl/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ppp--ppp_synctty.ko-entry_point_false-unreach-call.cil.out.c:6332: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-kgC5Fl/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ppp--ppp_synctty.ko-entry_point_false-unreach-call.cil.out.c:6320: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 9305 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-kgC5Fl/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ppp--ppp_synctty.ko-entry_point_false-unreach-call.cil.out.c:6241: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 13061 states (over memory cap)
KLEE: WARNING: killing 9248 states (over memory cap)
KLEE: WARNING: killing 13252 states (over memory cap)
KLEE: WARNING: killing 9465 states (over memory cap)
KLEE: WARNING: killing 9447 states (over memory cap)
KLEE: WARNING: killing 9518 states (over memory cap)
KLEE: WARNING: killing 9502 states (over memory cap)
KLEE: WARNING: killing 9660 states (over memory cap)
KLEE: WARNING: killing 9188 states (over memory cap)
KLEE: WARNING: killing 9715 states (over memory cap)
KLEE: WARNING: killing 9510 states (over memory cap)
KLEE: WARNING: killing 9396 states (over memory cap)
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 9741 states (over memory cap)
KLEE: WARNING: killing 9451 states (over memory cap)
KLEE: WARNING: killing 9614 states (over memory cap)
KLEE: WARNING: killing 9683 states (over memory cap)
KLEE: WARNING: killing 9752 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-kgC5Fl/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ppp--ppp_synctty.ko-entry_point_false-unreach-call.cil.out.c:5879: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 9726 states (over memory cap)
KLEE: WARNING: killing 9616 states (over memory cap)
KLEE: WARNING: killing 9597 states (over memory cap)
KLEE: WARNING: killing 9846 states (over memory cap)
KLEE: WARNING: killing 9567 states (over memory cap)
KLEE: WARNING: killing 9988 states (over memory cap)
KLEE: WARNING: killing 9617 states (over memory cap)
KLEE: WARNING: killing 9774 states (over memory cap)
KLEE: WARNING: killing 9667 states (over memory cap)
KLEE: WARNING: killing 9909 states (over memory cap)
KLEE: WARNING: killing 9544 states (over memory cap)
KLEE: WARNING: killing 9788 states (over memory cap)
KLEE: WARNING: killing 10120 states (over memory cap)
KLEE: WARNING: killing 9838 states (over memory cap)
KLEE: WARNING: killing 10166 states (over memory cap)
KLEE: WARNING: killing 9797 states (over memory cap)
KLEE: WARNING: killing 9868 states (over memory cap)
KLEE: WARNING: killing 9849 states (over memory cap)
KLEE: WARNING: killing 9832 states (over memory cap)
KLEE: WARNING: killing 9812 states (over memory cap)
KLEE: WARNING: killing 9619 states (over memory cap)
KLEE: WARNING: killing 9945 states (over memory cap)
KLEE: WARNING: killing 10011 states (over memory cap)
KLEE: WARNING: killing 9819 states (over memory cap)
KLEE: WARNING: killing 9715 states (over memory cap)
KLEE: WARNING: killing 9870 states (over memory cap)
KLEE: WARNING: killing 9853 states (over memory cap)
KLEE: WARNING: killing 10005 states (over memory cap)
KLEE: WARNING: killing 9905 states (over memory cap)
KLEE: WARNING: killing 9799 states (over memory cap)
KLEE: WARNING: killing 9870 states (over memory cap)
KLEE: WARNING: killing 10022 states (over memory cap)
KLEE: WARNING: killing 10172 states (over memory cap)
KLEE: WARNING: killing 9820 states (over memory cap)
KLEE: WARNING: killing 9801 states (over memory cap)
KLEE: WARNING: killing 9950 states (over memory cap)
KLEE: WARNING: killing 9515 states (over memory cap)
KLEE: WARNING: killing 9665 states (over memory cap)
KLEE: WARNING: killing 10064 states (over memory cap)
KLEE: WARNING: killing 10129 states (over memory cap)
KLEE: WARNING: killing 10032 states (over memory cap)
KLEE: WARNING: killing 9936 states (over memory cap)
KLEE: WARNING: killing 9750 states (over memory cap)
KLEE: WARNING: killing 9983 states (over memory cap)
KLEE: WARNING: killing 9801 states (over memory cap)
KLEE: WARNING: killing 10031 states (over memory cap)
KLEE: WARNING: killing 10096 states (over memory cap)
KLEE: WARNING: killing 9753 states (over memory cap)
KLEE: WARNING: killing 9737 states (over memory cap)
KLEE: WARNING: killing 9800 states (over memory cap)
KLEE: WARNING: killing 10030 states (over memory cap)
KLEE: WARNING: killing 10009 states (over memory cap)
KLEE: WARNING: killing 10244 states (over memory cap)
KLEE: WARNING: killing 10145 states (over memory cap)
KLEE: WARNING: killing 9807 states (over memory cap)
KLEE: WARNING: killing 10031 states (over memory cap)
KLEE: WARNING: killing 10177 states (over memory cap)
KLEE: WARNING: killing 10084 states (over memory cap)
KLEE: WARNING: killing 9740 states (over memory cap)
KLEE: WARNING: killing 9724 states (over memory cap)
KLEE: WARNING: killing 9871 states (over memory cap)
KLEE: WARNING: killing 10415 states (over memory cap)
KLEE: WARNING: killing 10165 states (over memory cap)
KLEE: WARNING: killing 10065 states (over memory cap)
KLEE: WARNING: killing 10048 states (over memory cap)
KLEE: WARNING: killing 10034 states (over memory cap)
KLEE: WARNING: killing 10016 states (over memory cap)
KLEE: WARNING: killing 9919 states (over memory cap)
