bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-32_7a-drivers--scsi--osst.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.: 218 212 3392 21494
Removed infinite loop in sg_page
Removed infinite loop in sg_assign_page
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.861712932587
Defining function snprintf as symbolic
Removed calls to '_raw_write_lock' (function is undefined)
Removed calls to '_raw_write_unlock' (function is undefined)
Removed calls to 'panic' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'sdev_prefix_printk' (function is undefined)
Removed calls to 'device_destroy' (function is undefined)
Removed calls to 'put_disk' (function is undefined)
Removed calls to 'vfree' (function is undefined)
Removed calls to '__free_pages' (function is undefined)
Defining function alloc_disk as symbolic
Defining function printk as symbolic
Defining function sprintf as symbolic
Defining function device_create as symbolic
Defining function device_create_file as symbolic
Defining function noop_llseek as symbolic
Removed calls to 'scsi_device_put' (function is undefined)
Defining function scsi_set_medium_removal as symbolic
Removed calls to 'msleep' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'blk_rq_set_block_pc' (function is undefined)
Removed calls to 'blk_put_request' (function is undefined)
Removed calls to 'blk_execute_rq_nowait' (function is undefined)
Removed calls to 'wait_for_completion' (function is undefined)
Removed calls to '__scsi_print_sense' (function is undefined)
Defining function scsi_normalize_sense as symbolic
Defining function scsi_get_sense_info_fld as symbolic
Defining function scsi_sense_desc_find as symbolic
Defining function blk_get_request as symbolic
Defining function sg_next as symbolic
Defining function blk_rq_map_user as symbolic
Defining function blk_rq_map_kern as symbolic
Removed calls to 'complete' (function is undefined)
Removed calls to '__blk_put_request' (function is undefined)
Defining function blk_rq_unmap_user as symbolic
Defining function jiffies_to_msecs as symbolic
Defining function vmalloc as symbolic
Defining function schedule_timeout_interruptible as symbolic
Defining function __msecs_to_jiffies as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function scsi_device_get as symbolic
Defining function scsi_block_when_processing_errors as symbolic
Defining function strlcpy as symbolic
Defining function alloc_pages_current as symbolic
Defining function scsi_ioctl_block_when_processing_errors as symbolic
Removed calls to '__might_fault' (function is undefined)
Removed calls to '__copy_from_user_overflow' (function is undefined)
Defining function capable as symbolic
Removed calls to '__copy_to_user_overflow' (function is undefined)
Defining function scsi_ioctl as symbolic
Defining function _copy_to_user as symbolic
Defining function _copy_from_user as symbolic
Defining function mutex_lock_interruptible as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'driver_remove_file' (function is undefined)
Removed calls to 'driver_unregister' (function is undefined)
Removed calls to '__unregister_chrdev' (function is undefined)
Removed calls to 'class_destroy' (function is undefined)
Defining function scsi_register_driver as symbolic
Defining function driver_create_file as symbolic
Defining function __register_chrdev as symbolic
Defining function __class_create as symbolic
Defining function mutex_trylock as symbolic
Linked our definitions to these undefined functions:
  memcmp
  strcpy
  strlen
  strncmp
  __kmalloc
  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.925108194351
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 312 199 1959 11847
INFO: Starting verification
KLEE: WARNING ONCE: function "sg_page" has inline asm
KLEE: WARNING ONCE: function "osst_do_scsi" has inline asm
KLEE: WARNING ONCE: function "sg_set_page" 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_0836869f-87f9-43c9-bdb4-18d6aaa654ad/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-G9hAd1/linux-4.2-rc1.tar.xz-32_7a-drivers--scsi--osst.ko-entry_point_true-unreach-call.cil.out.c:10550: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-G9hAd1/linux-4.2-rc1.tar.xz-32_7a-drivers--scsi--osst.ko-entry_point_true-unreach-call.cil.out.c:11978: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-G9hAd1/linux-4.2-rc1.tar.xz-32_7a-drivers--scsi--osst.ko-entry_point_true-unreach-call.cil.out.c:8841: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 7553 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 14862 states (over memory cap)
KLEE: WARNING: killing 14226 states (over memory cap)
KLEE: WARNING: killing 13742 states (over memory cap)
KLEE: WARNING: killing 13334 states (over memory cap)
KLEE: WARNING: killing 12782 states (over memory cap)
KLEE: WARNING: killing 13711 states (over memory cap)
KLEE: WARNING: killing 13608 states (over memory cap)
KLEE: WARNING: killing 13362 states (over memory cap)
KLEE: WARNING: killing 13330 states (over memory cap)
KLEE: WARNING: killing 14626 states (over memory cap)
KLEE: WARNING: killing 14970 states (over memory cap)
KLEE: WARNING: killing 15093 states (over memory cap)
KLEE: WARNING: killing 14922 states (over memory cap)
KLEE: WARNING: killing 15046 states (over memory cap)
KLEE: WARNING: killing 15465 states (over memory cap)
KLEE: WARNING: killing 15735 states (over memory cap)
KLEE: WARNING: killing 15933 states (over memory cap)
KLEE: WARNING: killing 15407 states (over memory cap)
KLEE: WARNING: killing 15828 states (over memory cap)
KLEE: WARNING: killing 15224 states (over memory cap)
KLEE: WARNING: killing 15422 states (over memory cap)
KLEE: WARNING: killing 15256 states (over memory cap)
KLEE: WARNING: killing 15094 states (over memory cap)
KLEE: WARNING: killing 14781 states (over memory cap)
KLEE: WARNING: killing 14114 states (over memory cap)
KLEE: WARNING: killing 14818 states (over memory cap)
KLEE: WARNING: killing 15008 states (over memory cap)
KLEE: WARNING: killing 14841 states (over memory cap)
KLEE: WARNING: killing 14751 states (over memory cap)
KLEE: WARNING: killing 14801 states (over memory cap)
KLEE: WARNING: killing 14142 states (over memory cap)
KLEE: WARNING: killing 14976 states (over memory cap)
KLEE: WARNING: killing 14674 states (over memory cap)
KLEE: WARNING: killing 15295 states (over memory cap)
KLEE: WARNING: killing 14854 states (over memory cap)
KLEE: WARNING: killing 15119 states (over memory cap)
KLEE: WARNING: killing 14243 states (over memory cap)
KLEE: WARNING: killing 14583 states (over memory cap)
KLEE: WARNING: killing 15131 states (over memory cap)
KLEE: WARNING: killing 14829 states (over memory cap)
KLEE: WARNING: killing 15310 states (over memory cap)
KLEE: WARNING: killing 14583 states (over memory cap)
KLEE: WARNING: killing 14422 states (over memory cap)
KLEE: WARNING: killing 14548 states (over memory cap)
KLEE: WARNING: killing 15166 states (over memory cap)
KLEE: WARNING: killing 14515 states (over memory cap)
KLEE: WARNING: killing 14635 states (over memory cap)
KLEE: WARNING: killing 15253 states (over memory cap)
KLEE: WARNING: killing 14812 states (over memory cap)
KLEE: WARNING: killing 14723 states (over memory cap)
KLEE: WARNING: killing 14427 states (over memory cap)
KLEE: WARNING: killing 14831 states (over memory cap)
KLEE: WARNING: killing 14399 states (over memory cap)
KLEE: WARNING: killing 15076 states (over memory cap)
KLEE: WARNING: killing 14991 states (over memory cap)
KLEE: WARNING: killing 14557 states (over memory cap)
KLEE: WARNING: killing 14609 states (over memory cap)
KLEE: WARNING: killing 14385 states (over memory cap)
KLEE: WARNING: killing 14854 states (over memory cap)
KLEE: WARNING: killing 14558 states (over memory cap)
KLEE: WARNING: killing 14824 states (over memory cap)
KLEE: WARNING: killing 15295 states (over memory cap)
KLEE: WARNING: killing 14930 states (over memory cap)
KLEE: WARNING: killing 14845 states (over memory cap)
KLEE: WARNING: killing 15246 states (over memory cap)
KLEE: WARNING: killing 15373 states (over memory cap)
KLEE: WARNING: killing 15221 states (over memory cap)
KLEE: WARNING: killing 15479 states (over memory cap)
KLEE: WARNING: killing 14642 states (over memory cap)
KLEE: WARNING: killing 14216 states (over memory cap)
KLEE: WARNING: killing 14062 states (over memory cap)
KLEE: WARNING: killing 14454 states (over memory cap)
KLEE: WARNING: killing 14775 states (over memory cap)
KLEE: WARNING: killing 14485 states (over memory cap)
KLEE: WARNING: killing 14873 states (over memory cap)
KLEE: WARNING: killing 14999 states (over memory cap)
KLEE: WARNING: killing 14772 states (over memory cap)
KLEE: WARNING: killing 14900 states (over memory cap)
KLEE: WARNING: killing 14954 states (over memory cap)
KLEE: WARNING: killing 15758 states (over memory cap)
KLEE: WARNING: killing 14589 states (over memory cap)
KLEE: WARNING: killing 14783 states (over memory cap)
KLEE: WARNING: killing 14833 states (over memory cap)
KLEE: WARNING: killing 14957 states (over memory cap)
KLEE: WARNING: killing 15015 states (over memory cap)
KLEE: WARNING: killing 14794 states (over memory cap)
KLEE: WARNING: killing 14852 states (over memory cap)
KLEE: WARNING: killing 15172 states (over memory cap)
KLEE: WARNING: killing 15032 states (over memory cap)
KLEE: WARNING: killing 14544 states (over memory cap)
KLEE: WARNING: killing 15271 states (over memory cap)
KLEE: WARNING: killing 14720 states (over memory cap)
KLEE: WARNING: killing 14371 states (over memory cap)
KLEE: WARNING: killing 14759 states (over memory cap)
KLEE: WARNING: killing 15207 states (over memory cap)
KLEE: WARNING: killing 14331 states (over memory cap)
KLEE: WARNING: killing 14986 states (over memory cap)
KLEE: WARNING: killing 14633 states (over memory cap)
KLEE: WARNING: killing 14421 states (over memory cap)
KLEE: WARNING: killing 14471 states (over memory cap)
KLEE: WARNING: killing 14654 states (over memory cap)
KLEE: WARNING: killing 14840 states (over memory cap)
KLEE: WARNING: killing 15097 states (over memory cap)
KLEE: WARNING: killing 14815 states (over memory cap)
KLEE: WARNING: killing 15604 states (over memory cap)
KLEE: WARNING: killing 14860 states (over memory cap)
KLEE: WARNING: killing 14649 states (over memory cap)
KLEE: WARNING: killing 14768 states (over memory cap)
KLEE: WARNING: killing 15022 states (over memory cap)
KLEE: WARNING: killing 14414 states (over memory cap)
KLEE: WARNING: killing 14997 states (over memory cap)
KLEE: WARNING: killing 15044 states (over memory cap)
KLEE: WARNING: killing 15038 states (over memory cap)
KLEE: WARNING: killing 14894 states (over memory cap)
KLEE: WARNING: killing 14615 states (over memory cap)
KLEE: WARNING: killing 14206 states (over memory cap)
KLEE: WARNING: killing 14255 states (over memory cap)
KLEE: WARNING: killing 15295 states (over memory cap)
KLEE: WARNING: killing 14885 states (over memory cap)
KLEE: WARNING: killing 14739 states (over memory cap)
KLEE: WARNING: killing 15127 states (over memory cap)
KLEE: WARNING: killing 14194 states (over memory cap)
KLEE: WARNING: killing 14640 states (over memory cap)
KLEE: WARNING: killing 15079 states (over memory cap)
KLEE: WARNING: killing 14744 states (over memory cap)
KLEE: WARNING: killing 15059 states (over memory cap)
KLEE: WARNING: killing 14530 states (over memory cap)
KLEE: WARNING: killing 14771 states (over memory cap)
KLEE: WARNING: killing 15022 states (over memory cap)
KLEE: WARNING: killing 15012 states (over memory cap)
KLEE: WARNING: killing 15587 states (over memory cap)
KLEE: WARNING: killing 15188 states (over memory cap)
KLEE: WARNING: killing 14001 states (over memory cap)
KLEE: WARNING: killing 14507 states (over memory cap)
KLEE: WARNING: killing 15074 states (over memory cap)
KLEE: WARNING: killing 14995 states (over memory cap)
KLEE: WARNING: killing 14727 states (over memory cap)
KLEE: WARNING: killing 14658 states (over memory cap)
KLEE: WARNING: killing 14969 states (over memory cap)
KLEE: WARNING: killing 15021 states (over memory cap)
KLEE: WARNING: killing 14297 states (over memory cap)
KLEE: WARNING: killing 14609 states (over memory cap)
KLEE: WARNING: killing 14917 states (over memory cap)
KLEE: WARNING: killing 15035 states (over memory cap)
KLEE: WARNING: killing 15084 states (over memory cap)
KLEE: WARNING: killing 14559 states (over memory cap)
KLEE: WARNING: killing 15257 states (over memory cap)
KLEE: WARNING: killing 14346 states (over memory cap)
KLEE: WARNING: killing 14521 states (over memory cap)
KLEE: WARNING: killing 14574 states (over memory cap)
KLEE: WARNING: killing 14883 states (over memory cap)
KLEE: WARNING: killing 14685 states (over memory cap)
KLEE: WARNING: killing 15312 states (over memory cap)
KLEE: WARNING: killing 14079 states (over memory cap)
KLEE: WARNING: killing 15731 states (over memory cap)
KLEE: WARNING: killing 14697 states (over memory cap)
KLEE: WARNING: killing 15320 states (over memory cap)
KLEE: WARNING: killing 15438 states (over memory cap)
KLEE: WARNING: killing 14794 states (over memory cap)
KLEE: WARNING: killing 14649 states (over memory cap)
KLEE: WARNING: killing 14325 states (over memory cap)
KLEE: WARNING: killing 14813 states (over memory cap)
KLEE: WARNING: killing 14612 states (over memory cap)
KLEE: WARNING: killing 14982 states (over memory cap)
KLEE: WARNING: killing 14969 states (over memory cap)
KLEE: WARNING: killing 14581 states (over memory cap)
KLEE: WARNING: killing 14820 states (over memory cap)
KLEE: WARNING: killing 14488 states (over memory cap)
KLEE: WARNING: killing 14346 states (over memory cap)
KLEE: WARNING: killing 15220 states (over memory cap)
KLEE: WARNING: killing 14898 states (over memory cap)
KLEE: WARNING: killing 15005 states (over memory cap)
KLEE: WARNING: killing 14932 states (over memory cap)
KLEE: WARNING: killing 15044 states (over memory cap)
KLEE: WARNING: killing 14782 states (over memory cap)
KLEE: WARNING: killing 14586 states (over memory cap)
KLEE: WARNING: killing 14316 states (over memory cap)
