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-43_2a-drivers--md--dm-crypt.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.: 142 222 1642 10519
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.419632911682
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 'mutex_lock_nested' (function is undefined)
Removed calls to 'bio_put' (function is undefined)
Removed calls to 'mutex_unlock' (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 _cond_resched as symbolic
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Removed calls to 'complete' (function is undefined)
Defining function bio_alloc_bioset as symbolic
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)
Removed calls to 'ldv_check_final_state' (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 ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  strchr
  strcmp
  strlen
  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.433662176132
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 250 165 956 6395
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_930b5397-89b4-4d71-a97e-e12733fb587d/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-GuD05M/linux-4.2-rc1.tar.xz-43_2a-drivers--md--dm-crypt.ko-entry_point_true-unreach-call.cil.out.c:9473: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-GuD05M/linux-4.2-rc1.tar.xz-43_2a-drivers--md--dm-crypt.ko-entry_point_true-unreach-call.cil.out.c:6054: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-GuD05M/linux-4.2-rc1.tar.xz-43_2a-drivers--md--dm-crypt.ko-entry_point_true-unreach-call.cil.out.c:5657: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-GuD05M/linux-4.2-rc1.tar.xz-43_2a-drivers--md--dm-crypt.ko-entry_point_true-unreach-call.cil.out.c:8513: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-GuD05M/linux-4.2-rc1.tar.xz-43_2a-drivers--md--dm-crypt.ko-entry_point_true-unreach-call.cil.out.c:6340: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-GuD05M/linux-4.2-rc1.tar.xz-43_2a-drivers--md--dm-crypt.ko-entry_point_true-unreach-call.cil.out.c:6320: 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-GuD05M/linux-4.2-rc1.tar.xz-43_2a-drivers--md--dm-crypt.ko-entry_point_true-unreach-call.cil.out.c:6541: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-GuD05M/linux-4.2-rc1.tar.xz-43_2a-drivers--md--dm-crypt.ko-entry_point_true-unreach-call.cil.out.c:6568: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-GuD05M/linux-4.2-rc1.tar.xz-43_2a-drivers--md--dm-crypt.ko-entry_point_true-unreach-call.cil.out.c:5657: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 11211 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 14099 states (over memory cap)
KLEE: WARNING: killing 13265 states (over memory cap)
KLEE: WARNING: killing 13402 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-GuD05M/linux-4.2-rc1.tar.xz-43_2a-drivers--md--dm-crypt.ko-entry_point_true-unreach-call.cil.out.c:5657: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 13256 states (over memory cap)
KLEE: WARNING: killing 13399 states (over memory cap)
KLEE: WARNING: killing 13598 states (over memory cap)
KLEE: WARNING: killing 13284 states (over memory cap)
KLEE: WARNING: killing 13540 states (over memory cap)
KLEE: WARNING: killing 13511 states (over memory cap)
KLEE: WARNING: killing 13996 states (over memory cap)
KLEE: WARNING: killing 15213 states (over memory cap)
KLEE: WARNING: killing 15137 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-GuD05M/linux-4.2-rc1.tar.xz-43_2a-drivers--md--dm-crypt.ko-entry_point_true-unreach-call.cil.out.c:6054: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15342 states (over memory cap)
KLEE: WARNING: killing 14371 states (over memory cap)
KLEE: WARNING: killing 14746 states (over memory cap)
KLEE: WARNING: killing 14671 states (over memory cap)
KLEE: WARNING: killing 14545 states (over memory cap)
KLEE: WARNING: killing 15198 states (over memory cap)
KLEE: WARNING: killing 14448 states (over memory cap)
KLEE: WARNING: killing 14379 states (over memory cap)
KLEE: WARNING: killing 13916 states (over memory cap)
KLEE: WARNING: killing 14786 states (over memory cap)
KLEE: WARNING: killing 14599 states (over memory cap)
KLEE: WARNING: killing 13967 states (over memory cap)
KLEE: WARNING: killing 14668 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-GuD05M/linux-4.2-rc1.tar.xz-43_2a-drivers--md--dm-crypt.ko-entry_point_true-unreach-call.cil.out.c:5668: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 14145 states (over memory cap)
KLEE: WARNING: killing 14242 states (over memory cap)
KLEE: WARNING: killing 14004 states (over memory cap)
KLEE: WARNING: killing 14149 states (over memory cap)
KLEE: WARNING: killing 14078 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 14337 states (over memory cap)
KLEE: WARNING: killing 13991 states (over memory cap)
KLEE: WARNING: killing 14462 states (over memory cap)
KLEE: WARNING: killing 14061 states (over memory cap)
KLEE: WARNING: killing 14701 states (over memory cap)
KLEE: WARNING: killing 14301 states (over memory cap)
KLEE: WARNING: killing 14614 states (over memory cap)
KLEE: WARNING: killing 14438 states (over memory cap)
KLEE: WARNING: killing 14148 states (over memory cap)
KLEE: WARNING: killing 14289 states (over memory cap)
KLEE: WARNING: killing 14166 states (over memory cap)
KLEE: WARNING: killing 14579 states (over memory cap)
KLEE: WARNING: killing 14511 states (over memory cap)
KLEE: WARNING: killing 14497 states (over memory cap)
KLEE: WARNING: killing 14429 states (over memory cap)
KLEE: WARNING: killing 14411 states (over memory cap)
KLEE: WARNING: killing 14237 states (over memory cap)
KLEE: WARNING: killing 13465 states (over memory cap)
KLEE: WARNING: killing 14304 states (over memory cap)
KLEE: WARNING: killing 14513 states (over memory cap)
KLEE: WARNING: killing 14118 states (over memory cap)
KLEE: WARNING: killing 14155 states (over memory cap)
KLEE: WARNING: killing 14787 states (over memory cap)
KLEE: WARNING: killing 13864 states (over memory cap)
KLEE: WARNING: killing 14542 states (over memory cap)
KLEE: WARNING: killing 14315 states (over memory cap)
KLEE: WARNING: killing 14354 states (over memory cap)
KLEE: WARNING: killing 14872 states (over memory cap)
KLEE: WARNING: killing 14650 states (over memory cap)
KLEE: WARNING: killing 14318 states (over memory cap)
KLEE: WARNING: killing 13561 states (over memory cap)
KLEE: WARNING: killing 14287 states (over memory cap)
KLEE: WARNING: killing 14811 states (over memory cap)
KLEE: WARNING: killing 14581 states (over memory cap)
KLEE: WARNING: killing 14407 states (over memory cap)
KLEE: WARNING: killing 13969 states (over memory cap)
KLEE: WARNING: killing 13798 states (over memory cap)
KLEE: WARNING: killing 14044 states (over memory cap)
KLEE: WARNING: killing 14347 states (over memory cap)
KLEE: WARNING: killing 14333 states (over memory cap)
KLEE: WARNING: killing 14326 states (over memory cap)
KLEE: WARNING: killing 14308 states (over memory cap)
KLEE: WARNING: killing 14193 states (over memory cap)
KLEE: WARNING: killing 14290 states (over memory cap)
KLEE: WARNING: killing 13539 states (over memory cap)
KLEE: WARNING: killing 13890 states (over memory cap)
KLEE: WARNING: killing 14402 states (over memory cap)
KLEE: WARNING: killing 13494 states (over memory cap)
KLEE: WARNING: killing 14740 states (over memory cap)
KLEE: WARNING: killing 14992 states (over memory cap)
KLEE: WARNING: killing 14563 states (over memory cap)
KLEE: WARNING: killing 15072 states (over memory cap)
KLEE: WARNING: killing 13964 states (over memory cap)
KLEE: WARNING: killing 14002 states (over memory cap)
KLEE: WARNING: killing 14349 states (over memory cap)
KLEE: WARNING: killing 14864 states (over memory cap)
KLEE: WARNING: killing 14799 states (over memory cap)
KLEE: WARNING: killing 13801 states (over memory cap)
KLEE: WARNING: killing 13888 states (over memory cap)
KLEE: WARNING: killing 14496 states (over memory cap)
KLEE: WARNING: killing 13918 states (over memory cap)
KLEE: WARNING: killing 14108 states (over memory cap)
KLEE: WARNING: killing 14099 states (over memory cap)
KLEE: WARNING: killing 15327 states (over memory cap)
KLEE: WARNING: killing 14020 states (over memory cap)
KLEE: WARNING: killing 14269 states (over memory cap)
KLEE: WARNING: killing 14049 states (over memory cap)
KLEE: WARNING: killing 14600 states (over memory cap)
KLEE: WARNING: killing 14228 states (over memory cap)
KLEE: WARNING: killing 14629 states (over memory cap)
KLEE: WARNING: killing 14724 states (over memory cap)
KLEE: WARNING: killing 13994 states (over memory cap)
KLEE: WARNING: killing 13828 states (over memory cap)
KLEE: WARNING: killing 13762 states (over memory cap)
KLEE: WARNING: killing 14259 states (over memory cap)
KLEE: WARNING: killing 13841 states (over memory cap)
KLEE: WARNING: killing 15008 states (over memory cap)
KLEE: WARNING: killing 14176 states (over memory cap)
KLEE: WARNING: killing 14372 states (over memory cap)
KLEE: WARNING: killing 14560 states (over memory cap)
KLEE: WARNING: killing 14090 states (over memory cap)
KLEE: WARNING: killing 14838 states (over memory cap)
KLEE: WARNING: killing 14067 states (over memory cap)
KLEE: WARNING: killing 14873 states (over memory cap)
KLEE: WARNING: killing 14050 states (over memory cap)
KLEE: WARNING: killing 14496 states (over memory cap)
KLEE: WARNING: killing 14631 states (over memory cap)
KLEE: WARNING: killing 14371 states (over memory cap)
KLEE: WARNING: killing 14258 states (over memory cap)
KLEE: WARNING: killing 13948 states (over memory cap)
KLEE: WARNING: killing 13574 states (over memory cap)
KLEE: WARNING: killing 14826 states (over memory cap)
KLEE: WARNING: killing 14210 states (over memory cap)
KLEE: WARNING: killing 14148 states (over memory cap)
KLEE: WARNING: killing 14283 states (over memory cap)
KLEE: WARNING: killing 14268 states (over memory cap)
KLEE: WARNING: killing 14312 states (over memory cap)
KLEE: WARNING: killing 14093 states (over memory cap)
KLEE: WARNING: killing 13580 states (over memory cap)
KLEE: WARNING: killing 13869 states (over memory cap)
KLEE: WARNING: killing 14510 states (over memory cap)
KLEE: WARNING: killing 14844 states (over memory cap)
KLEE: WARNING: killing 14887 states (over memory cap)
KLEE: WARNING: killing 13974 states (over memory cap)
KLEE: WARNING: killing 14058 states (over memory cap)
KLEE: WARNING: killing 14951 states (over memory cap)
KLEE: WARNING: killing 14389 states (over memory cap)
KLEE: WARNING: killing 14431 states (over memory cap)
KLEE: WARNING: killing 13369 states (over memory cap)
KLEE: WARNING: killing 14300 states (over memory cap)
KLEE: WARNING: killing 14297 states (over memory cap)
KLEE: WARNING: killing 14578 states (over memory cap)
KLEE: WARNING: killing 14271 states (over memory cap)
KLEE: WARNING: killing 13211 states (over memory cap)
KLEE: WARNING: killing 13645 states (over memory cap)
KLEE: WARNING: killing 14227 states (over memory cap)
KLEE: WARNING: killing 14119 states (over memory cap)
KLEE: WARNING: killing 14504 states (over memory cap)
KLEE: WARNING: killing 14292 states (over memory cap)
KLEE: WARNING: killing 14232 states (over memory cap)
KLEE: WARNING: killing 14620 states (over memory cap)
KLEE: WARNING: killing 14508 states (over memory cap)
KLEE: WARNING: killing 13409 states (over memory cap)
KLEE: WARNING: killing 14975 states (over memory cap)
KLEE: WARNING: killing 14378 states (over memory cap)
KLEE: WARNING: killing 14317 states (over memory cap)
KLEE: WARNING: killing 14509 states (over memory cap)
KLEE: WARNING: killing 14449 states (over memory cap)
KLEE: WARNING: killing 13943 states (over memory cap)
KLEE: WARNING: killing 13976 states (over memory cap)
KLEE: WARNING: killing 14204 states (over memory cap)
KLEE: WARNING: killing 13896 states (over memory cap)
KLEE: WARNING: killing 13639 states (over memory cap)
KLEE: WARNING: killing 14262 states (over memory cap)
KLEE: WARNING: killing 14104 states (over memory cap)
KLEE: WARNING: killing 14042 states (over memory cap)
KLEE: WARNING: killing 14470 states (over memory cap)
KLEE: WARNING: killing 13972 states (over memory cap)
KLEE: WARNING: killing 14650 states (over memory cap)
KLEE: WARNING: killing 14980 states (over memory cap)
KLEE: WARNING: killing 13841 states (over memory cap)
KLEE: WARNING: killing 14762 states (over memory cap)
KLEE: WARNING: killing 14602 states (over memory cap)
KLEE: WARNING: killing 14587 states (over memory cap)
KLEE: WARNING: killing 14631 states (over memory cap)
KLEE: WARNING: killing 13986 states (over memory cap)
KLEE: WARNING: killing 14211 states (over memory cap)
KLEE: WARNING: killing 13911 states (over memory cap)
KLEE: WARNING: killing 13944 states (over memory cap)
KLEE: WARNING: killing 14417 states (over memory cap)
KLEE: WARNING: killing 14600 states (over memory cap)
KLEE: WARNING: killing 14103 states (over memory cap)
