bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main2_sequence_infinite_withcheck_stateful.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.: 62 318 1886 14756
Removed infinite loop in node_prepare_for_write
Removed infinite loop in sm_disk_new_block
Removed infinite loop in dm_btree_remove
Removed infinite loop in shadow_current
Removed infinite loop in __find_holder
Removed infinite loop in shadow_parent
Removed infinite loop in dm_tm_inc
Removed infinite loop in delete_at
Removed infinite loop in dm_tm_dec
Removed infinite loop in __rebalance3
Removed infinite loop in delete_center_node
Removed infinite loop in redistribute3
Removed infinite loop in shift
Removed infinite loop in node_shift
Removed infinite loop in node_copy
Removed infinite loop in bl_up_read
Removed infinite loop in __wake_many
Removed infinite loop in ro_node
INFO: Compilation, preparation and instrumentation time: 0.502964019775
Defining function ___ratelimit as symbolic
Defining function printk as symbolic
Defining function crc32c as symbolic
Defining function dm_bufio_get_block_number as symbolic
Defining function dm_bufio_get_block_data as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function dm_bufio_get_block_size as symbolic
Removed calls to 'dm_bufio_release' (function is undefined)
Defining function dm_bufio_new as symbolic
Defining function dm_bufio_get_aux_data as symbolic
Removed calls to '__list_add' (function is undefined)
Removed calls to 'print_stack_trace' (function is undefined)
Removed calls to 'save_stack_trace' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to '__put_task_struct' (function is undefined)
Defining function dm_bufio_read as symbolic
Removed calls to 'list_del' (function is undefined)
Defining function wake_up_process as symbolic
Defining function dm_bufio_get as symbolic
Removed calls to 'dm_bufio_mark_buffer_dirty' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Defining function dm_bufio_client_create as symbolic
Defining function dm_bufio_get_client as symbolic
Removed calls to 'dm_bufio_client_destroy' (function is undefined)
Defining function dm_bufio_get_device_size as symbolic
Defining function dm_bufio_write_dirty_buffers as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function mutex_trylock as symbolic
Removed calls to 'ldv_handler_precall' (function is undefined)
Linked our definitions to these undefined functions:
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 0.53000998497
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 164 262 1285 9157
INFO: Starting verification
KLEE: WARNING ONCE: function "node_prepare_for_write" has inline asm
KLEE: WARNING ONCE: function "sm_disk_new_block" has inline asm
KLEE: WARNING ONCE: function "sm_ll_find_free_block" has inline asm
KLEE: WARNING ONCE: function "sm_ll_insert" has inline asm
KLEE: WARNING ONCE: function "dm_btree_remove" has inline asm
KLEE: WARNING ONCE: function "shadow_current" has inline asm
KLEE: WARNING ONCE: function "shadow_parent" has inline asm
KLEE: WARNING ONCE: function "bl_down_write" has inline asm
KLEE: WARNING ONCE: function "__check_holder" has inline asm
KLEE: WARNING ONCE: function "__add_holder" has inline asm
KLEE: WARNING ONCE: function "__wait" has inline asm
KLEE: WARNING ONCE: function "put_task_struct" has inline asm
KLEE: WARNING ONCE: function "__find_holder" has inline asm
KLEE: WARNING ONCE: function "dm_tm_inc" has inline asm
KLEE: WARNING ONCE: function "delete_at" has inline asm
KLEE: WARNING ONCE: function "dm_tm_dec" has inline asm
KLEE: WARNING ONCE: function "node_copy" has inline asm
KLEE: WARNING ONCE: function "node_shift" has inline asm
KLEE: WARNING ONCE: function "shift" has inline asm
KLEE: WARNING ONCE: function "dm_bm_read_try_lock" has inline asm
KLEE: WARNING ONCE: function "dm_bm_read_lock" has inline asm
KLEE: WARNING ONCE: function "bl_up_read" has inline asm
KLEE: WARNING ONCE: function "__wake_many" has inline asm
KLEE: WARNING ONCE: function "bl_up_write" has inline asm
KLEE: WARNING ONCE: function "sm_ll_lookup_bitmap" has inline asm
KLEE: WARNING ONCE: function "ro_node" has inline asm
KLEE: WARNING ONCE: flushing 9576 bytes on read, may be slow and/or crash: MO53[9576] allocated at global:
KLEE: ERROR: /tmp/symbiotic-8VmGrR/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c:6215: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8VmGrR/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c:6215: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8VmGrR/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c:6233: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8VmGrR/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c:6232: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_8c59c294-5041-47f2-8867-50dd627fb2df/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_8c59c294-5041-47f2-8867-50dd627fb2df/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_8c59c294-5041-47f2-8867-50dd627fb2df/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_8c59c294-5041-47f2-8867-50dd627fb2df/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_8c59c294-5041-47f2-8867-50dd627fb2df/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_8c59c294-5041-47f2-8867-50dd627fb2df/symbiotic/lib/kernel/kfree.c:5: free of alloca
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8VmGrR/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c:6010: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8VmGrR/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c:6010: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8VmGrR/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c:6215: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8VmGrR/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c:6215: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8VmGrR/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c:5998: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8VmGrR/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c:5998: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8VmGrR/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c:5998: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8VmGrR/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c:5998: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8VmGrR/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c:5998: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8VmGrR/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c:5998: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8VmGrR/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c:6010: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8VmGrR/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c:6010: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8VmGrR/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c:6231: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8VmGrR/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c:6010: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8VmGrR/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c:5490: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8VmGrR/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c:5203: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8VmGrR/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c:6010: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8VmGrR/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c:5204: divide by zero
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8VmGrR/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c:5135: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8VmGrR/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c:5136: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8VmGrR/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c:5207: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8VmGrR/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c:6143: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8VmGrR/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c:5491: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8VmGrR/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c:5142: divide by zero
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8VmGrR/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c:6143: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8VmGrR/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c:5148: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_8c59c294-5041-47f2-8867-50dd627fb2df/symbiotic/lib/kernel/__memcpy.c:7: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8VmGrR/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c:6230: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8VmGrR/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c:6010: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8VmGrR/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c:6010: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8VmGrR/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c:6010: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8VmGrR/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c:6010: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8VmGrR/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c:5364: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8VmGrR/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c:5491: invalid function pointer
KLEE: NOTE: now ignoring this error at this location
