bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--mmc--card--mmc_test.ko_true-unreach-call.cil.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.: 172 685 3381 18104
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_linux_kernel_module_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 0.805154085159
Removed calls to '_dev_info' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to 'debugfs_remove' (function is undefined)
Removed calls to 'dev_err' (function is undefined)
Removed calls to 'ldv_after_alloc' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Defining function debugfs_create_file as symbolic
Defining function external_allocated_data as symbolic
Removed calls to 'sg_init_one' (function is undefined)
Removed calls to 'getnstimeofday64' (function is undefined)
Defining function mmc_can_reset as symbolic
Defining function mmc_hw_reset as symbolic
Defining function mmc_can_erase as symbolic
Defining function mmc_erase as symbolic
Removed calls to 'sg_init_table' (function is undefined)
Defining function printk as symbolic
Removed calls to 'set_normalized_timespec' (function is undefined)
Removed calls to 'mmc_wait_for_req' (function is undefined)
Removed calls to 'mmc_set_data_timeout' (function is undefined)
Defining function mmc_wait_for_cmd as symbolic
Defining function mmc_start_req as symbolic
Defining function sg_next as symbolic
Defining function __phys_addr as symbolic
Defining function mmc_can_trim as symbolic
Defining function nr_free_buffer_pages as symbolic
Removed calls to '__free_pages' (function is undefined)
Defining function mmc_set_blocklen as symbolic
Removed calls to 'trace_hardirqs_off' (function is undefined)
Removed calls to 'trace_hardirqs_on' (function is undefined)
Defining function sg_copy_from_buffer as symbolic
Defining function sg_copy_to_buffer as symbolic
Defining function seq_lseek as symbolic
Defining function seq_read as symbolic
Removed calls to 'mmc_release_host' (function is undefined)
Defining function single_release as symbolic
Defining function single_open as symbolic
Defining function seq_printf as symbolic
Defining function kstrtol_from_user as symbolic
Defining function __mmc_claim_host as symbolic
Removed calls to 'mmc_unregister_driver' (function is undefined)
Defining function mmc_register_driver as symbolic
Removed calls to 'ldv_assert' (function is undefined)
Linked our definitions to these undefined functions:
  __memset
  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.8889939785
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 265 659 2420 12263
INFO: Starting verification
KLEE: WARNING ONCE: function "mmc_test_area_io_seq" has inline asm
KLEE: WARNING ONCE: function "sg_set_page" has inline asm
KLEE: WARNING ONCE: function "mmc_test_prepare_mrq" has inline asm
KLEE: WARNING ONCE: function "mmc_test_check_result" has inline asm
KLEE: WARNING ONCE: function "mmc_test_area_init" has inline asm
KLEE: WARNING ONCE: function "mmc_test_broken_transfer" has inline asm
KLEE: WARNING ONCE: function "mmc_test_transfer" has inline asm
KLEE: WARNING ONCE: function "arch_local_irq_save" has inline asm
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: ERROR: /tmp/symbiotic-mpjavK/linux-4.0-rc1---drivers--mmc--card--mmc_test.ko_true-unreach-call.cil.c:8759: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_624fb9f4-9e85-47bb-ad04-679771097f61/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mpjavK/linux-4.0-rc1---drivers--mmc--card--mmc_test.ko_true-unreach-call.cil.c:6764: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mpjavK/linux-4.0-rc1---drivers--mmc--card--mmc_test.ko_true-unreach-call.cil.c:6926: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_624fb9f4-9e85-47bb-ad04-679771097f61/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_624fb9f4-9e85-47bb-ad04-679771097f61/symbiotic/lib/kernel/kfree.c:5: free of global
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mpjavK/linux-4.0-rc1---drivers--mmc--card--mmc_test.ko_true-unreach-call.cil.c:6926: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
