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--md--dm-crypt.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.: 145 259 1836 11094
Removed infinite loop in sg_page
Removed infinite loop in kcryptd_crypt_write_io_submit
Removed infinite loop in crypt_free_buffer_pages
Removed infinite loop in sg_assign_page
Removed infinite loop in dmcrypt_write
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.449965000153
Removed calls to 'kzfree' (function is undefined)
Removed calls to 'sg_init_one' (function is undefined)
Defining function crypto_alloc_base as symbolic
Removed calls to 'crypto_destroy_tfm' (function is undefined)
Removed calls to 'crypto_xor' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function crypto_shash_update as symbolic
Defining function crypto_alloc_shash as symbolic
Removed calls to 'memzero_explicit' (function is undefined)
Defining function crypto_shash_final as symbolic
Removed calls to '__mutex_init' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'destroy_workqueue' (function is undefined)
Removed calls to 'bioset_free' (function is undefined)
Removed calls to 'mempool_destroy' (function is undefined)
Removed calls to 'dm_put_device' (function is undefined)
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Defining function strcasecmp as symbolic
Defining function printk as symbolic
Defining function kstrtou8 as symbolic
Defining function scnprintf as symbolic
Removed calls to 'generic_make_request' (function is undefined)
Removed calls to 'bio_put' (function is undefined)
Defining function queue_work_on as symbolic
Removed calls to 'wait_for_completion' (function is undefined)
Removed calls to '___might_sleep' (function is undefined)
Removed calls to 'sg_init_table' (function is undefined)
Removed calls to 'rb_insert_color' (function is undefined)
Removed calls to '__wake_up_locked' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'mempool_free' (function is undefined)
Removed calls to 'bio_endio' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Defining function _cond_resched as symbolic
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Defining function mempool_alloc as symbolic
Removed calls to 'complete' (function is undefined)
Removed calls to 'mutex_lock' (function is undefined)
Defining function bio_alloc_bioset as symbolic
Removed calls to 'mutex_unlock' (function is undefined)
Defining function bio_clone_fast as symbolic
Defining function kthread_stop as symbolic
Defining function bioset_create as symbolic
Defining function sscanf as symbolic
Defining function dm_table_get_mode as symbolic
Defining function dm_get_device as symbolic
Defining function dm_read_arg_group as symbolic
Defining function dm_shift_arg as symbolic
Defining function __alloc_workqueue_key as symbolic
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Removed calls to 'remove_wait_queue' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to 'blk_start_plug' (function is undefined)
Removed calls to 'rb_erase' (function is undefined)
Removed calls to 'blk_finish_plug' (function is undefined)
Defining function kthread_create_on_node as symbolic
Defining function wake_up_process as symbolic
Defining function default_wake_function as symbolic
Defining function kthread_should_stop as symbolic
Defining function rb_first as symbolic
Defining function __bitmap_weight as symbolic
Defining function mempool_alloc_pages as symbolic
Defining function mempool_create as symbolic
Defining function mempool_kmalloc as symbolic
Defining function kstrdup as symbolic
Defining function strsep as symbolic
Defining function snprintf as symbolic
Defining function crypto_alloc_ablkcipher as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'dm_unregister_target' (function is undefined)
Defining function ldv_presuspend_3 as symbolic
Defining function ldv_release_8 as symbolic
Defining function ldv_setup_8 as symbolic
Defining function ldv_release_4 as symbolic
Defining function ldv_setup_4 as symbolic
Defining function ldv_release_5 as symbolic
Defining function ldv_setup_5 as symbolic
Defining function dm_register_target as symbolic
Defining function queue_delayed_work_on as symbolic
Removed calls to 'flush_workqueue' (function is undefined)
Defining function mutex_trylock as symbolic
Linked our definitions to these undefined functions:
  strchr
  strcmp
  strlen
  __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.45524096489
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 255 205 1114 6783
INFO: Starting verification
KLEE: WARNING ONCE: function "crypt_iv_benbi_ctr" has inline asm
KLEE: WARNING ONCE: function "crypt_iv_lmk_gen" has inline asm
KLEE: WARNING ONCE: function "crypt_iv_lmk_post" has inline asm
KLEE: WARNING ONCE: function "sg_page" has inline asm
KLEE: WARNING ONCE: function "__kunmap_atomic" has inline asm
KLEE: WARNING ONCE: function "crypt_iv_tcw_gen" has inline asm
KLEE: WARNING ONCE: function "crypt_iv_tcw_post" has inline asm
KLEE: WARNING ONCE: function "crypt_ctr" has inline asm
KLEE: WARNING ONCE: function "crypt_postsuspend" has inline asm
KLEE: WARNING ONCE: function "crypt_resume" has inline asm
KLEE: WARNING ONCE: function "crypt_message" has inline asm
KLEE: WARNING ONCE: function "crypt_set_key" has inline asm
KLEE: WARNING ONCE: function "crypt_setkey_allcpus" has inline asm
KLEE: WARNING ONCE: function "kcryptd_io_read" has inline asm
KLEE: WARNING ONCE: function "kcryptd_io_read_work" has inline asm
KLEE: WARNING ONCE: function "kcryptd_crypt" has inline asm
KLEE: WARNING ONCE: function "crypt_convert" has inline asm
KLEE: WARNING ONCE: function "crypt_dec_pending" has inline asm
KLEE: WARNING ONCE: function "crypt_free_buffer_pages" has inline asm
KLEE: WARNING ONCE: function "kcryptd_crypt_write_io_submit" has inline asm
KLEE: WARNING ONCE: function "kcryptd_async_done" has inline asm
KLEE: WARNING ONCE: function "sg_set_page" has inline asm
KLEE: WARNING ONCE: function "dmcrypt_write" has inline asm
KLEE: WARNING ONCE: function "main" has inline asm
KLEE: WARNING: undefined reference to function: mempool_free_pages
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_30eb5c3d-bc5e-4008-998a-f7ce3d1b93f5/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-1NNeRu/linux-4.2-rc1.tar.xz-32_7a-drivers--md--dm-crypt.ko-entry_point_false-unreach-call.cil.out.c:9488: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-1NNeRu/linux-4.2-rc1.tar.xz-32_7a-drivers--md--dm-crypt.ko-entry_point_false-unreach-call.cil.out.c:6554: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-1NNeRu/linux-4.2-rc1.tar.xz-32_7a-drivers--md--dm-crypt.ko-entry_point_false-unreach-call.cil.out.c:5684: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-1NNeRu/linux-4.2-rc1.tar.xz-32_7a-drivers--md--dm-crypt.ko-entry_point_false-unreach-call.cil.out.c:8528: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-1NNeRu/linux-4.2-rc1.tar.xz-32_7a-drivers--md--dm-crypt.ko-entry_point_false-unreach-call.cil.out.c:6581: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-1NNeRu/linux-4.2-rc1.tar.xz-32_7a-drivers--md--dm-crypt.ko-entry_point_false-unreach-call.cil.out.c:5684: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-1NNeRu/linux-4.2-rc1.tar.xz-32_7a-drivers--md--dm-crypt.ko-entry_point_false-unreach-call.cil.out.c:6333: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-1NNeRu/linux-4.2-rc1.tar.xz-32_7a-drivers--md--dm-crypt.ko-entry_point_false-unreach-call.cil.out.c:6067: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 14429 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: ERROR: /tmp/symbiotic-1NNeRu/linux-4.2-rc1.tar.xz-32_7a-drivers--md--dm-crypt.ko-entry_point_false-unreach-call.cil.out.c:6353: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 14280 states (over memory cap)
KLEE: WARNING: killing 13958 states (over memory cap)
KLEE: WARNING: killing 13068 states (over memory cap)
KLEE: WARNING: killing 13670 states (over memory cap)
KLEE: WARNING: killing 13865 states (over memory cap)
KLEE: WARNING: killing 13782 states (over memory cap)
KLEE: WARNING: killing 13473 states (over memory cap)
KLEE: WARNING: killing 13616 states (over memory cap)
KLEE: WARNING: killing 14094 states (over memory cap)
KLEE: WARNING: killing 14919 states (over memory cap)
KLEE: WARNING: killing 15120 states (over memory cap)
KLEE: WARNING: killing 14993 states (over memory cap)
KLEE: WARNING: killing 15476 states (over memory cap)
KLEE: WARNING: killing 15912 states (over memory cap)
KLEE: WARNING: killing 15270 states (over memory cap)
KLEE: WARNING: killing 14809 states (over memory cap)
KLEE: WARNING: killing 15514 states (over memory cap)
KLEE: WARNING: killing 15499 states (over memory cap)
KLEE: WARNING: killing 13919 states (over memory cap)
KLEE: WARNING: killing 14625 states (over memory cap)
KLEE: WARNING: killing 14159 states (over memory cap)
KLEE: WARNING: killing 14525 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 14284 states (over memory cap)
KLEE: WARNING: killing 14542 states (over memory cap)
KLEE: WARNING: killing 14359 states (over memory cap)
KLEE: WARNING: killing 14503 states (over memory cap)
KLEE: WARNING: killing 14753 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-1NNeRu/linux-4.2-rc1.tar.xz-32_7a-drivers--md--dm-crypt.ko-entry_point_false-unreach-call.cil.out.c:5684: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 14569 states (over memory cap)
KLEE: WARNING: killing 15441 states (over memory cap)
KLEE: WARNING: killing 14648 states (over memory cap)
KLEE: WARNING: killing 14686 states (over memory cap)
KLEE: WARNING: killing 14778 states (over memory cap)
KLEE: WARNING: killing 14377 states (over memory cap)
KLEE: WARNING: killing 14689 states (over memory cap)
KLEE: WARNING: killing 15061 states (over memory cap)
KLEE: WARNING: killing 14986 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-1NNeRu/linux-4.2-rc1.tar.xz-32_7a-drivers--md--dm-crypt.ko-entry_point_false-unreach-call.cil.out.c:5695: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 14474 states (over memory cap)
KLEE: WARNING: killing 14628 states (over memory cap)
KLEE: WARNING: killing 14884 states (over memory cap)
KLEE: WARNING: killing 14322 states (over memory cap)
KLEE: WARNING: killing 14630 states (over memory cap)
KLEE: WARNING: killing 14614 states (over memory cap)
KLEE: WARNING: killing 14056 states (over memory cap)
KLEE: WARNING: killing 14521 states (over memory cap)
KLEE: WARNING: killing 14887 states (over memory cap)
KLEE: WARNING: killing 15035 states (over memory cap)
KLEE: WARNING: killing 14150 states (over memory cap)
KLEE: WARNING: killing 14731 states (over memory cap)
KLEE: WARNING: killing 14279 states (over memory cap)
KLEE: WARNING: killing 15024 states (over memory cap)
KLEE: WARNING: killing 14363 states (over memory cap)
KLEE: WARNING: killing 15473 states (over memory cap)
KLEE: WARNING: killing 14491 states (over memory cap)
KLEE: WARNING: killing 14959 states (over memory cap)
KLEE: WARNING: killing 14730 states (over memory cap)
KLEE: WARNING: killing 14765 states (over memory cap)
KLEE: WARNING: killing 14482 states (over memory cap)
KLEE: WARNING: killing 15004 states (over memory cap)
KLEE: WARNING: killing 14567 states (over memory cap)
KLEE: WARNING: killing 14975 states (over memory cap)
KLEE: WARNING: killing 14754 states (over memory cap)
KLEE: WARNING: killing 14469 states (over memory cap)
KLEE: WARNING: killing 14507 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-1NNeRu/linux-4.2-rc1.tar.xz-32_7a-drivers--md--dm-crypt.ko-entry_point_false-unreach-call.cil.out.c:6067: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 14498 states (over memory cap)
KLEE: WARNING: killing 14372 states (over memory cap)
KLEE: WARNING: killing 14520 states (over memory cap)
KLEE: WARNING: killing 14818 states (over memory cap)
KLEE: WARNING: killing 13855 states (over memory cap)
KLEE: WARNING: killing 14690 states (over memory cap)
KLEE: WARNING: killing 14672 states (over memory cap)
KLEE: WARNING: killing 14767 states (over memory cap)
KLEE: WARNING: killing 14806 states (over memory cap)
KLEE: WARNING: killing 14634 states (over memory cap)
KLEE: WARNING: killing 15147 states (over memory cap)
KLEE: WARNING: killing 13981 states (over memory cap)
KLEE: WARNING: killing 15331 states (over memory cap)
KLEE: WARNING: killing 14164 states (over memory cap)
KLEE: WARNING: killing 14935 states (over memory cap)
KLEE: WARNING: killing 15077 states (over memory cap)
KLEE: WARNING: killing 14440 states (over memory cap)
KLEE: WARNING: killing 14219 states (over memory cap)
KLEE: WARNING: killing 14671 states (over memory cap)
KLEE: WARNING: killing 14498 states (over memory cap)
KLEE: WARNING: killing 13965 states (over memory cap)
KLEE: WARNING: killing 15053 states (over memory cap)
KLEE: WARNING: killing 14622 states (over memory cap)
KLEE: WARNING: killing 14505 states (over memory cap)
KLEE: WARNING: killing 14491 states (over memory cap)
KLEE: WARNING: killing 14846 states (over memory cap)
KLEE: WARNING: killing 14522 states (over memory cap)
KLEE: WARNING: killing 15492 states (over memory cap)
KLEE: WARNING: killing 14600 states (over memory cap)
KLEE: WARNING: killing 14437 states (over memory cap)
KLEE: WARNING: killing 14994 states (over memory cap)
KLEE: WARNING: killing 14307 states (over memory cap)
KLEE: WARNING: killing 15176 states (over memory cap)
KLEE: WARNING: killing 14543 states (over memory cap)
KLEE: WARNING: killing 14476 states (over memory cap)
KLEE: WARNING: killing 14618 states (over memory cap)
KLEE: WARNING: killing 14508 states (over memory cap)
KLEE: WARNING: killing 14079 states (over memory cap)
KLEE: WARNING: killing 15101 states (over memory cap)
KLEE: WARNING: killing 14573 states (over memory cap)
KLEE: WARNING: killing 14561 states (over memory cap)
KLEE: WARNING: killing 14547 states (over memory cap)
KLEE: WARNING: killing 14587 states (over memory cap)
KLEE: WARNING: killing 14727 states (over memory cap)
KLEE: WARNING: killing 14205 states (over memory cap)
KLEE: WARNING: killing 14701 states (over memory cap)
KLEE: WARNING: killing 14696 states (over memory cap)
KLEE: WARNING: killing 14936 states (over memory cap)
KLEE: WARNING: killing 13847 states (over memory cap)
KLEE: WARNING: killing 14555 states (over memory cap)
KLEE: WARNING: killing 15150 states (over memory cap)
KLEE: WARNING: killing 14785 states (over memory cap)
KLEE: WARNING: killing 14521 states (over memory cap)
KLEE: WARNING: killing 14963 states (over memory cap)
KLEE: WARNING: killing 14294 states (over memory cap)
KLEE: WARNING: killing 14690 states (over memory cap)
KLEE: WARNING: killing 14019 states (over memory cap)
KLEE: WARNING: killing 15376 states (over memory cap)
KLEE: WARNING: killing 14147 states (over memory cap)
KLEE: WARNING: killing 14739 states (over memory cap)
KLEE: WARNING: killing 15188 states (over memory cap)
KLEE: WARNING: killing 14519 states (over memory cap)
KLEE: WARNING: killing 14754 states (over memory cap)
KLEE: WARNING: killing 14845 states (over memory cap)
KLEE: WARNING: killing 14280 states (over memory cap)
KLEE: WARNING: killing 14464 states (over memory cap)
KLEE: WARNING: killing 14657 states (over memory cap)
KLEE: WARNING: killing 14844 states (over memory cap)
KLEE: WARNING: killing 14882 states (over memory cap)
KLEE: WARNING: killing 14172 states (over memory cap)
KLEE: WARNING: killing 14359 states (over memory cap)
KLEE: WARNING: killing 14899 states (over memory cap)
KLEE: WARNING: killing 14388 states (over memory cap)
KLEE: WARNING: killing 14625 states (over memory cap)
KLEE: WARNING: killing 14615 states (over memory cap)
KLEE: WARNING: killing 14953 states (over memory cap)
KLEE: WARNING: killing 14586 states (over memory cap)
KLEE: WARNING: killing 14475 states (over memory cap)
KLEE: WARNING: killing 14259 states (over memory cap)
KLEE: WARNING: killing 14944 states (over memory cap)
KLEE: WARNING: killing 14086 states (over memory cap)
KLEE: WARNING: killing 14670 states (over memory cap)
KLEE: WARNING: killing 14508 states (over memory cap)
KLEE: WARNING: killing 14846 states (over memory cap)
KLEE: WARNING: killing 14886 states (over memory cap)
KLEE: WARNING: killing 14975 states (over memory cap)
KLEE: WARNING: killing 14613 states (over memory cap)
KLEE: WARNING: killing 15100 states (over memory cap)
KLEE: WARNING: killing 14485 states (over memory cap)
KLEE: WARNING: killing 14227 states (over memory cap)
KLEE: WARNING: killing 14464 states (over memory cap)
KLEE: WARNING: killing 14992 states (over memory cap)
KLEE: WARNING: killing 14440 states (over memory cap)
KLEE: WARNING: killing 14475 states (over memory cap)
KLEE: WARNING: killing 14512 states (over memory cap)
KLEE: WARNING: killing 14893 states (over memory cap)
KLEE: WARNING: killing 15131 states (over memory cap)
KLEE: WARNING: killing 14379 states (over memory cap)
KLEE: WARNING: killing 13723 states (over memory cap)
KLEE: WARNING: killing 14738 states (over memory cap)
KLEE: WARNING: killing 14879 states (over memory cap)
KLEE: WARNING: killing 14222 states (over memory cap)
KLEE: WARNING: killing 14749 states (over memory cap)
KLEE: WARNING: killing 14888 states (over memory cap)
KLEE: WARNING: killing 14333 states (over memory cap)
KLEE: WARNING: killing 14811 states (over memory cap)
KLEE: WARNING: killing 14702 states (over memory cap)
KLEE: WARNING: killing 14741 states (over memory cap)
KLEE: WARNING: killing 14435 states (over memory cap)
KLEE: WARNING: killing 14083 states (over memory cap)
