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-08_1a-drivers--md--dm-cache.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.: 205 409 2625 19323
Removed infinite loop in set_discard
Removed infinite loop in get_per_bio_data
Removed infinite loop in prealloc_get_migration
Removed infinite loop in inc_ds
Removed infinite loop in prealloc_get_cell
Removed infinite loop in prealloc_put_cell
Removed infinite loop in process_flush_bio
Removed infinite loop in null_locker
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 0.663959980011
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function printk as symbolic
Removed calls to '__list_del_entry' (function is undefined)
Defining function __request_module as symbolic
Removed calls to 'dm_consume_args' (function is undefined)
Removed calls to 'dm_table_add_target_callbacks' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to 'init_timer_key' (function is undefined)
Removed calls to 'down_read' (function is undefined)
Removed calls to 'up_read' (function is undefined)
Removed calls to 'dm_put_device' (function is undefined)
Removed calls to 'bio_endio' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'dm_deferred_entry_dec' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to 'flush_workqueue' (function is undefined)
Removed calls to 'dm_cell_error' (function is undefined)
Removed calls to 'dm_bio_prison_free_cell' (function is undefined)
Removed calls to 'blk_limits_io_min' (function is undefined)
Removed calls to 'blk_limits_io_opt' (function is undefined)
Defining function strcasecmp as symbolic
Defining function kstrtoull as symbolic
Defining function prepare_to_wait_event as symbolic
Defining function queue_work_on as symbolic
Defining function sscanf as symbolic
Defining function dm_table_get_md as symbolic
Defining function dm_device_name as symbolic
Defining function scnprintf as symbolic
Defining function dm_suspended as symbolic
Defining function sprintf as symbolic
Removed calls to 'down_write' (function is undefined)
Removed calls to 'up_write' (function is undefined)
Defining function ___ratelimit as symbolic
Removed calls to 'dm_table_event' (function is undefined)
Removed calls to 'dm_bm_set_read_only' (function is undefined)
Removed calls to 'dm_bm_set_read_write' (function is undefined)
Defining function dm_bm_is_read_only as symbolic
Removed calls to 'dm_tm_destroy' (function is undefined)
Removed calls to 'dm_block_manager_destroy' (function is undefined)
Removed calls to 'dm_disk_bitset_init' (function is undefined)
Defining function dm_block_manager_create as symbolic
Defining function dm_block_data as symbolic
Defining function dm_tm_open_with_sm as symbolic
Removed calls to 'dm_array_info_init' (function is undefined)
Defining function dm_bm_unlock as symbolic
Defining function dm_bm_read_lock as symbolic
Defining function dm_tm_create_with_sm as symbolic
Defining function dm_array_empty as symbolic
Defining function dm_bitset_empty as symbolic
Defining function dm_tm_pre_commit as symbolic
Defining function dm_tm_commit as symbolic
Defining function dm_bm_write_lock_zero as symbolic
Defining function dm_bm_block_size as symbolic
Defining function dm_bm_write_lock as symbolic
Defining function dm_bitset_flush as symbolic
Defining function queue_delayed_work_on as symbolic
Defining function _raw_spin_lock_irqsave as symbolic
Defining function dm_bitset_test_bit as symbolic
Defining function dm_array_walk as symbolic
Defining function dm_array_get_value as symbolic
Defining function dm_array_resize as symbolic
Defining function dm_array_set_value as symbolic
Defining function dm_array_del as symbolic
Defining function dm_bitset_clear_bit as symbolic
Defining function dm_bitset_set_bit as symbolic
Defining function dm_bitset_resize as symbolic
Removed calls to 'generic_make_request' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Removed calls to 'dm_cell_release' (function is undefined)
Removed calls to 'mempool_free' (function is undefined)
Defining function dm_cell_promote_or_release as symbolic
Defining function dm_kcopyd_copy as symbolic
Removed calls to 'dm_cell_visit_release' (function is undefined)
Defining function dm_deferred_set_add_work as symbolic
Defining function dm_deferred_entry_inc as symbolic
Defining function dm_bio_detain as symbolic
Defining function dm_bio_prison_alloc_cell as symbolic
Defining function mempool_alloc as symbolic
Defining function dm_get_cell as symbolic
Defining function cancel_delayed_work as symbolic
Removed calls to 'mempool_destroy' (function is undefined)
Removed calls to 'dm_deferred_set_destroy' (function is undefined)
Removed calls to 'dm_bio_prison_destroy' (function is undefined)
Removed calls to 'destroy_workqueue' (function is undefined)
Removed calls to 'vfree' (function is undefined)
Removed calls to 'dm_kcopyd_client_destroy' (function is undefined)
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function kstrdup as symbolic
Defining function dm_set_target_max_io_len as symbolic
Removed calls to '__init_rwsem' (function is undefined)
Defining function dm_kcopyd_client_create as symbolic
Defining function __alloc_workqueue_key as symbolic
Defining function dm_bio_prison_create as symbolic
Defining function dm_deferred_set_create as symbolic
Defining function mempool_alloc_slab as symbolic
Defining function mempool_create as symbolic
Defining function vzalloc as symbolic
Defining function dm_bm_flush as symbolic
Defining function dm_shift_arg as symbolic
Defining function dm_read_arg_group as symbolic
Defining function dm_get_device as symbolic
Defining function bdevname as symbolic
Defining function dm_block_location as symbolic
Defining function dm_bm_checksum as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'dm_unregister_target' (function is undefined)
Removed calls to 'kmem_cache_destroy' (function is undefined)
Defining function ldv_presuspend_4 as symbolic
Defining function ldv_release_3 as symbolic
Defining function ldv_probe_3 as symbolic
Defining function dm_register_target as symbolic
Defining function kmem_cache_create as symbolic
Linked our definitions to these undefined functions:
  strcmp
  strlen
  strncmp
  strncpy
  __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.732598781586
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 320 248 1546 11178
INFO: Starting verification
KLEE: WARNING ONCE: function "cache_ctr" has inline asm
KLEE: WARNING ONCE: function "cache_map" has inline asm
KLEE: WARNING ONCE: function "cache_end_io" has inline asm
KLEE: WARNING ONCE: function "cache_postsuspend" has inline asm
KLEE: WARNING ONCE: function "cache_preresume" has inline asm
KLEE: WARNING ONCE: function "commit" has inline asm
KLEE: WARNING ONCE: function "dm_cache_metadata_set_needs_check" has inline asm
KLEE: WARNING ONCE: function "set_clean_shutdown" has inline asm
KLEE: WARNING ONCE: function "clear_clean_shutdown" has inline asm
KLEE: WARNING ONCE: function "set_discard" has inline asm
KLEE: WARNING ONCE: function "set_dirty" has inline asm
KLEE: WARNING ONCE: function "clear_dirty" has inline asm
KLEE: WARNING ONCE: function "do_worker" has inline asm
KLEE: WARNING ONCE: function "prealloc_get_cell" has inline asm
KLEE: WARNING ONCE: function "prealloc_data_structs" has inline asm
KLEE: WARNING ONCE: function "accounted_begin" has inline asm
KLEE: WARNING ONCE: function "prealloc_put_cell" has inline asm
KLEE: WARNING ONCE: function "process_cell" has inline asm
KLEE: WARNING ONCE: function "issue_copy_or_discard" has inline asm
KLEE: WARNING ONCE: function "migration_failure" has inline asm
KLEE: WARNING ONCE: function "migration_success_post_commit" has inline asm
KLEE: WARNING ONCE: function "free_migration" has inline asm
KLEE: WARNING ONCE: function "migration_success_pre_commit" has inline asm
KLEE: WARNING ONCE: function "is_discarded_oblock" has inline asm
KLEE: WARNING ONCE: function "overwrite_endio" has inline asm
KLEE: WARNING ONCE: function "check_if_tick_bio_needed" has inline asm
KLEE: WARNING ONCE: function "prealloc_get_migration" has inline asm
KLEE: WARNING ONCE: function "remap_to_origin_clear_discard" has inline asm
KLEE: WARNING ONCE: function "inc_ds" has inline asm
KLEE: WARNING ONCE: function "remap_to_origin_then_cache" has inline asm
KLEE: WARNING ONCE: function "remap_cell_to_cache_dirty" has inline asm
KLEE: WARNING ONCE: function "remap_cell_to_origin_clear_discard" has inline asm
KLEE: WARNING ONCE: function "writethrough_endio" has inline asm
KLEE: WARNING ONCE: function "null_locker" has inline asm
KLEE: WARNING ONCE: function "dm_cache_metadata_close" has inline asm
KLEE: WARNING ONCE: function "dm_cache_metadata_open" has inline asm
KLEE: WARNING: undefined reference to function: delayed_work_timer_fn
KLEE: WARNING: undefined reference to function: mempool_free_slab
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_35fda47e-26a0-47d7-9708-758929a2dee3/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Un5GuT/linux-4.2-rc1.tar.xz-08_1a-drivers--md--dm-cache.ko-entry_point_false-unreach-call.cil.out.c:10657: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Un5GuT/linux-4.2-rc1.tar.xz-08_1a-drivers--md--dm-cache.ko-entry_point_false-unreach-call.cil.out.c:10679: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Un5GuT/linux-4.2-rc1.tar.xz-08_1a-drivers--md--dm-cache.ko-entry_point_false-unreach-call.cil.out.c:11939: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Un5GuT/linux-4.2-rc1.tar.xz-08_1a-drivers--md--dm-cache.ko-entry_point_false-unreach-call.cil.out.c:9619: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Un5GuT/linux-4.2-rc1.tar.xz-08_1a-drivers--md--dm-cache.ko-entry_point_false-unreach-call.cil.out.c:11947: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Un5GuT/linux-4.2-rc1.tar.xz-08_1a-drivers--md--dm-cache.ko-entry_point_false-unreach-call.cil.out.c:10716: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Un5GuT/linux-4.2-rc1.tar.xz-08_1a-drivers--md--dm-cache.ko-entry_point_false-unreach-call.cil.out.c:11956: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Un5GuT/linux-4.2-rc1.tar.xz-08_1a-drivers--md--dm-cache.ko-entry_point_false-unreach-call.cil.out.c:10178: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Un5GuT/linux-4.2-rc1.tar.xz-08_1a-drivers--md--dm-cache.ko-entry_point_false-unreach-call.cil.out.c:11904: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Un5GuT/linux-4.2-rc1.tar.xz-08_1a-drivers--md--dm-cache.ko-entry_point_false-unreach-call.cil.out.c:11904: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Un5GuT/linux-4.2-rc1.tar.xz-08_1a-drivers--md--dm-cache.ko-entry_point_false-unreach-call.cil.out.c:11905: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Un5GuT/linux-4.2-rc1.tar.xz-08_1a-drivers--md--dm-cache.ko-entry_point_false-unreach-call.cil.out.c:11959: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
