bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-net-ppp_generic.ko_false-unreach-call.cil.out.i.pp.i


--------------------------------------------------------------------------------


5.0.0-KLEE:86e6f6f8-dg:03407af1-symbiotic:a8aa8ad6-minisat:3db58943-stp:17249213-sbt-instrumentation:dd7e4312
INFO: After compilation stats: Globals/Functions/Blocks/Instr.: 68 157 1886 10193
Removed infinite loop in __skb_pull
Removed infinite loop in skb_queue_next
Removed infinite loop in net_generic
Removed infinite loop in ppp_pernet
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 0.416991949081
Removed calls to 'kfree_skb' (function is undefined)
Removed calls to '_raw_read_lock_bh' (function is undefined)
Removed calls to 'skb_queue_tail' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Removed calls to '_raw_read_unlock_bh' (function is undefined)
Defining function skb_dequeue as symbolic
Removed calls to '_raw_spin_lock_bh' (function is undefined)
Removed calls to '_raw_spin_unlock_bh' (function is undefined)
Removed calls to 'skb_trim' (function is undefined)
Defining function dev_alloc_skb as symbolic
Defining function netdev_err as symbolic
Defining function skb_put as symbolic
Defining function skb_copy_bits as symbolic
Defining function slhc_uncompress as symbolic
Defining function netdev_printk as symbolic
Defining function slhc_remember as symbolic
Defining function pskb_expand_head as symbolic
Defining function skb_push as symbolic
Defining function sk_run_filter as symbolic
Defining function skb_pull_rcsum as symbolic
Defining function netif_rx as symbolic
Defining function skb_pull as symbolic
Defining function slhc_toss as symbolic
Defining function __pskb_pull_tail as symbolic
Removed calls to 'idr_init' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'idr_destroy' (function is undefined)
Removed calls to 'lock_acquire' (function is undefined)
Removed calls to 'lockdep_rcu_dereference' (function is undefined)
Removed calls to 'lock_release' (function is undefined)
Defining function debug_lockdep_rcu_enabled as symbolic
Defining function lock_is_held as symbolic
Defining function noop_llseek as symbolic
Removed calls to 'add_wait_queue' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'remove_wait_queue' (function is undefined)
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'might_fault' (function is undefined)
Removed calls to 'idr_remove' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'free_netdev' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to '_raw_write_lock_bh' (function is undefined)
Removed calls to '_raw_write_unlock_bh' (function is undefined)
Removed calls to 'down_read' (function is undefined)
Removed calls to 'up_read' (function is undefined)
Removed calls to 'slhc_free' (function is undefined)
Removed calls to 'unregister_netdev' (function is undefined)
Removed calls to 'skb_queue_purge' (function is undefined)
Defining function printk as symbolic
Defining function capable as symbolic
Removed calls to 'list_del' (function is undefined)
Defining function slhc_init as symbolic
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Removed calls to '__netif_schedule' (function is undefined)
Defining function memdup_user as symbolic
Defining function sk_chk_filter as symbolic
Defining function netpoll_trap as symbolic
Defining function _copy_from_user as symbolic
Defining function _copy_to_user as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function __request_module as symbolic
Defining function ldv_undefined_int as symbolic
Defining function idr_find as symbolic
Defining function alloc_netdev_mqs as symbolic
Removed calls to '__init_waitqueue_head' (function is undefined)
Defining function sprintf as symbolic
Defining function register_netdev as symbolic
Defining function idr_pre_get as symbolic
Defining function idr_get_new_above as symbolic
Removed calls to 'skb_queue_head' (function is undefined)
Defining function slhc_compress as symbolic
Defining function net_ratelimit as symbolic
Defining function __alloc_skb as symbolic
Defining function default_wake_function as symbolic
Defining function skb_copy_datagram_iovec as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to '__init_rwsem' (function is undefined)
Removed calls to '__rwlock_init' (function is undefined)
Removed calls to 'down_write' (function is undefined)
Removed calls to 'up_write' (function is undefined)
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to '__unregister_chrdev' (function is undefined)
Removed calls to 'unregister_pernet_device' (function is undefined)
Removed calls to 'ldv_check_return_value' (function is undefined)
Removed calls to 'device_destroy' (function is undefined)
Removed calls to 'class_destroy' (function is undefined)
Defining function register_pernet_device as symbolic
Defining function __class_create as symbolic
Defining function device_create as symbolic
Defining function __register_chrdev as symbolic
Linked our definitions to these undefined functions:
  strlen
  __kmalloc
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 0.400450944901
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 162 108 807 5343
INFO: Starting verification
KLEE: WARNING ONCE: function "ppp_do_recv" has inline asm
KLEE: WARNING ONCE: function "ppp_receive_nonmp_frame" has inline asm
KLEE: WARNING ONCE: function "net_generic" has inline asm
KLEE: WARNING ONCE: function "ppp_read" has inline asm
KLEE: WARNING ONCE: function "ppp_ioctl" has inline asm
KLEE: WARNING ONCE: function "ppp_release" has inline asm
KLEE: WARNING ONCE: function "ppp_destroy_interface" has inline asm
KLEE: WARNING ONCE: function "ppp_destroy_channel" has inline asm
KLEE: WARNING ONCE: function "ppp_pernet" has inline asm
KLEE: WARNING ONCE: function "ppp_disconnect_channel" has inline asm
KLEE: WARNING ONCE: function "netif_wake_queue" has inline asm
KLEE: WARNING ONCE: function "ppp_start_xmit" has inline asm
KLEE: WARNING ONCE: function "ppp_register_channel" has inline asm
KLEE: WARNING ONCE: function "ppp_register_net_channel" has inline asm
KLEE: WARNING ONCE: function "ppp_unregister_channel" has inline asm
KLEE: WARNING ONCE: flushing 9608 bytes on read, may be slow and/or crash: MO17[9608] allocated at global:
KLEE: ERROR: /tmp/symbiotic-rqr0pY/module_get_put-drivers-net-ppp_generic.ko_false-unreach-call.cil.out.i.pp.i:7948: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-rqr0pY/module_get_put-drivers-net-ppp_generic.ko_false-unreach-call.cil.out.i.pp.i:6792: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-rqr0pY/module_get_put-drivers-net-ppp_generic.ko_false-unreach-call.cil.out.i.pp.i:6210: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-rqr0pY/module_get_put-drivers-net-ppp_generic.ko_false-unreach-call.cil.out.i.pp.i:5647: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-rqr0pY/module_get_put-drivers-net-ppp_generic.ko_false-unreach-call.cil.out.i.pp.i:6145: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-rqr0pY/module_get_put-drivers-net-ppp_generic.ko_false-unreach-call.cil.out.i.pp.i:6145: invalid function pointer
KLEE: NOTE: now ignoring this error at this location
