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-block-pktcdvd.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.: 171 161 1736 10437
Removed infinite loop in pkt_open
Removed infinite loop in pkt_close
Removed infinite loop in pkt_handle_queue
Removed infinite loop in pkt_run_state_machine
Removed infinite loop in pkt_gather_data
Removed infinite loop in pkt_start_write
Removed infinite loop in pkt_copy_bio_data
Removed infinite loop in pkt_make_local_copy
Removed infinite loop in pkt_end_io_packet_write
Removed infinite loop in pkt_bio_finished
Removed infinite loop in pkt_end_io_read
Removed infinite loop in pkt_rbtree_find
Removed infinite loop in pkt_get_packet_data
Removed infinite loop in pkt_rbtree_erase
Removed infinite loop in pkt_make_request
Removed infinite loop in pkt_merge_bvec
Removed infinite loop in pkt_shrink_pktlist
Removed infinite loop in pkt_grow_pktlist
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 0.419588804245
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'debugfs_remove' (function is undefined)
Removed calls to 'class_destroy' (function is undefined)
Removed calls to 'unregister_blkdev' (function is undefined)
Removed calls to 'mempool_destroy' (function is undefined)
Removed calls to 'ldv_check_return_value' (function is undefined)
Removed calls to 'remove_proc_entry' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'bd_set_size' (function is undefined)
Removed calls to 'init_cdrom_command' (function is undefined)
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to 'blk_queue_max_hw_sectors' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'bio_put' (function is undefined)
Removed calls to '__free_pages' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'might_fault' (function is undefined)
Defining function misc_deregister as symbolic
Defining function capable as symbolic
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'blk_queue_make_request' (function is undefined)
Removed calls to 'blk_queue_logical_block_size' (function is undefined)
Removed calls to 'blk_queue_merge_bvec' (function is undefined)
Removed calls to 'add_disk' (function is undefined)
Removed calls to 'blk_cleanup_queue' (function is undefined)
Removed calls to 'put_disk' (function is undefined)
Removed calls to 'kobject_put' (function is undefined)
Removed calls to 'device_unregister' (function is undefined)
Removed calls to 'del_gendisk' (function is undefined)
Defining function _copy_to_user as symbolic
Defining function printk as symbolic
Defining function kthread_stop as symbolic
Defining function blkdev_put as symbolic
Defining function sprintf as symbolic
Defining function alloc_disk as symbolic
Defining function blk_alloc_queue as symbolic
Defining function debugfs_create_dir as symbolic
Defining function debugfs_create_file as symbolic
Defining function device_create as symbolic
Defining function kobject_init_and_add as symbolic
Defining function kobject_uevent as symbolic
Defining function bdevname as symbolic
Defining function bdget as symbolic
Defining function blkdev_get as symbolic
Defining function set_blocksize as symbolic
Removed calls to 'set_user_nice' (function is undefined)
Removed calls to 'add_wait_queue' (function is undefined)
Removed calls to 'refrigerator' (function is undefined)
Removed calls to 'remove_wait_queue' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to 'rb_erase' (function is undefined)
Removed calls to 'mempool_free' (function is undefined)
Removed calls to 'clear_bdi_congested' (function is undefined)
Removed calls to 'bio_init' (function is undefined)
Removed calls to 'bio_endio' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to 'generic_make_request' (function is undefined)
Defining function kthread_create_on_node as symbolic
Defining function wake_up_process as symbolic
Defining function proc_create_data as symbolic
Defining function default_wake_function as symbolic
Defining function schedule_timeout as symbolic
Defining function kthread_should_stop as symbolic
Removed calls to 'blk_put_request' (function is undefined)
Defining function blk_get_request as symbolic
Defining function blk_rq_map_kern as symbolic
Defining function blk_execute_rq as symbolic
Removed calls to '__wake_up' (function is undefined)
Defining function bio_add_page as symbolic
Defining function rb_first as symbolic
Defining function rb_next as symbolic
Removed calls to 'blk_queue_bounce' (function is undefined)
Removed calls to 'bio_pair_release' (function is undefined)
Removed calls to 'set_bdi_congested' (function is undefined)
Removed calls to 'rb_insert_color' (function is undefined)
Defining function bio_clone as symbolic
Defining function mempool_alloc as symbolic
Defining function bio_split as symbolic
Defining function congestion_wait as symbolic
Defining function kasprintf as symbolic
Defining function mempool_kmalloc as symbolic
Defining function mempool_create as symbolic
Defining function _copy_from_user as symbolic
Defining function __blkdev_driver_ioctl as symbolic
Defining function alloc_pages_current as symbolic
Defining function single_open as symbolic
Defining function seq_printf as symbolic
Defining function sscanf as symbolic
Defining function register_blkdev as symbolic
Defining function misc_register as symbolic
Defining function proc_mkdir as symbolic
Defining function __class_register as symbolic
Defining function ldv_undefined_int as symbolic
Defining function seq_lseek as symbolic
Defining function seq_read as symbolic
Defining function single_release as symbolic
Defining function no_llseek as symbolic
Defining function nonseekable_open as symbolic
Linked our definitions to these undefined functions:
  strcmp
  strcpy
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 0.587728977203
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 285 108 798 7542
INFO: Starting verification
KLEE: WARNING ONCE: function "pkt_open" has inline asm
KLEE: WARNING ONCE: function "pkt_close" has inline asm
KLEE: WARNING ONCE: function "kcdrwd" has inline asm
KLEE: WARNING ONCE: function "pkt_rbtree_find" has inline asm
KLEE: WARNING ONCE: function "pkt_end_io_read" has inline asm
KLEE: WARNING ONCE: function "pkt_make_local_copy" has inline asm
KLEE: WARNING ONCE: function "pkt_end_io_packet_write" has inline asm
KLEE: WARNING ONCE: function "pkt_bio_finished" has inline asm
KLEE: WARNING ONCE: function "pkt_shrink_pktlist" has inline asm
KLEE: WARNING: undefined reference to function: mempool_kfree
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_4fd6d30d-a707-478b-a240-a2f124b63b3e/symbiotic/lib/kernel/kfree.c:5: memory error: invalid pointer: free
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_4fd6d30d-a707-478b-a240-a2f124b63b3e/symbiotic/lib/kernel/kfree.c:5: free of global
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_4fd6d30d-a707-478b-a240-a2f124b63b3e/symbiotic/lib/kernel/kfree.c:5: free of alloca
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: flushing 9608 bytes on read, may be slow and/or crash: MO17[9608] allocated at global:
KLEE: ERROR: /tmp/symbiotic-StiRDS/module_get_put-drivers-block-pktcdvd.ko_false-unreach-call.cil.out.i.pp.i:5159: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-StiRDS/module_get_put-drivers-block-pktcdvd.ko_false-unreach-call.cil.out.i.pp.i:4851: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-StiRDS/module_get_put-drivers-block-pktcdvd.ko_false-unreach-call.cil.out.i.pp.i:4509: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-StiRDS/module_get_put-drivers-block-pktcdvd.ko_false-unreach-call.cil.out.i.pp.i:4867: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_4fd6d30d-a707-478b-a240-a2f124b63b3e/symbiotic/lib/kernel/kfree.c:5: memory error: invalid pointer: free
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_4fd6d30d-a707-478b-a240-a2f124b63b3e/symbiotic/lib/kernel/kfree.c:5: free of global
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_4fd6d30d-a707-478b-a240-a2f124b63b3e/symbiotic/lib/kernel/kfree.c:5: free of alloca
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_4fd6d30d-a707-478b-a240-a2f124b63b3e/symbiotic/lib/libc/strcmp.c:3: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-StiRDS/module_get_put-drivers-block-pktcdvd.ko_false-unreach-call.cil.out.i.pp.i:9088: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-StiRDS/module_get_put-drivers-block-pktcdvd.ko_false-unreach-call.cil.out.i.pp.i:9307: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-StiRDS/module_get_put-drivers-block-pktcdvd.ko_false-unreach-call.cil.out.i.pp.i:4692: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-StiRDS/module_get_put-drivers-block-pktcdvd.ko_false-unreach-call.cil.out.i.pp.i:9248: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-StiRDS/module_get_put-drivers-block-pktcdvd.ko_false-unreach-call.cil.out.i.pp.i:9248: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-StiRDS/module_get_put-drivers-block-pktcdvd.ko_false-unreach-call.cil.out.i.pp.i:4756: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-StiRDS/module_get_put-drivers-block-pktcdvd.ko_false-unreach-call.cil.out.i.pp.i:9313: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_4fd6d30d-a707-478b-a240-a2f124b63b3e/symbiotic/lib/libc/strcmp.c:3: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-StiRDS/module_get_put-drivers-block-pktcdvd.ko_false-unreach-call.cil.out.i.pp.i:9272: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-StiRDS/module_get_put-drivers-block-pktcdvd.ko_false-unreach-call.cil.out.i.pp.i:9285: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
