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--iio--accel--kxcjk-1013.ko_false-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.: 104 528 1918 10549
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.549538135529
Removed calls to 'dev_err' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'pm_runtime_enable' (function is undefined)
Removed calls to 'pm_runtime_set_autosuspend_delay' (function is undefined)
Removed calls to '__pm_runtime_use_autosuspend' (function is undefined)
Removed calls to 'iio_device_unregister' (function is undefined)
Removed calls to 'iio_triggered_buffer_cleanup' (function is undefined)
Removed calls to 'iio_trigger_unregister' (function is undefined)
Removed calls to '__pm_runtime_disable' (function is undefined)
Defining function i2c_smbus_read_byte_data as symbolic
Defining function i2c_smbus_write_byte_data as symbolic
Defining function __pm_runtime_set_status as symbolic
Defining function devm_iio_device_alloc as symbolic
Removed calls to 'iio_trigger_poll' (function is undefined)
Defining function devm_iio_trigger_alloc as symbolic
Defining function iio_pollfunc_store_time as symbolic
Removed calls to 'iio_trigger_notify_done' (function is undefined)
Defining function iio_device_register as symbolic
Defining function iio_triggered_buffer_setup as symbolic
Defining function iio_push_to_buffers as symbolic
Defining function i2c_smbus_read_word_data as symbolic
Defining function iio_trigger_register as symbolic
Defining function __pm_runtime_suspend as symbolic
Defining function __pm_runtime_resume as symbolic
Defining function get_device as symbolic
Defining function devm_request_threaded_irq as symbolic
Defining function iio_push_event as symbolic
Defining function ktime_get_with_offset as symbolic
Defining function __devm_gpiod_get_index as symbolic
Defining function gpiod_direction_input as symbolic
Defining function gpiod_to_irq as symbolic
Defining function acpi_match_device as symbolic
Removed calls to 'usleep_range' (function is undefined)
Defining function msleep_interruptible as symbolic
Defining function iio_read_const_attr as symbolic
Defining function external_allocated_data as symbolic
Removed calls to 'i2c_del_driver' (function is undefined)
Defining function i2c_register_driver as symbolic
Removed calls to 'ldv_pre_probe' (function is undefined)
Removed calls to 'ldv_after_alloc' (function is undefined)
Removed calls to 'ldv_assert' (function is undefined)
Linked our definitions to these undefined functions:
  strcmp
  __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.583529949188
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 189 468 1688 6487
INFO: Starting verification
KLEE: WARNING ONCE: function "kxcjk1013_remove" has inline asm
KLEE: WARNING ONCE: function "kxcjk1013_set_power_state" has inline asm
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_d6a47fa2-1e9d-4c25-9633-f5bed26aa6e6/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-pKG4BY/linux-4.0-rc1---drivers--iio--accel--kxcjk-1013.ko_false-unreach-call.cil.c:6625: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-pKG4BY/linux-4.0-rc1---drivers--iio--accel--kxcjk-1013.ko_false-unreach-call.cil.c:6625: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-pKG4BY/linux-4.0-rc1---drivers--iio--accel--kxcjk-1013.ko_false-unreach-call.cil.c:6630: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-pKG4BY/linux-4.0-rc1---drivers--iio--accel--kxcjk-1013.ko_false-unreach-call.cil.c:6632: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-pKG4BY/linux-4.0-rc1---drivers--iio--accel--kxcjk-1013.ko_false-unreach-call.cil.c:6630: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-pKG4BY/linux-4.0-rc1---drivers--iio--accel--kxcjk-1013.ko_false-unreach-call.cil.c:6635: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-pKG4BY/linux-4.0-rc1---drivers--iio--accel--kxcjk-1013.ko_false-unreach-call.cil.c:8229: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-pKG4BY/linux-4.0-rc1---drivers--iio--accel--kxcjk-1013.ko_false-unreach-call.cil.c:7934: invalid function pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: output directory is "/tmp/symbiotic-pKG4BY/klee-out-0"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: function "kxcjk1013_remove" has inline asm
KLEE: WARNING ONCE: function "kxcjk1013_set_power_state" has inline asm
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_d6a47fa2-1e9d-4c25-9633-f5bed26aa6e6/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-pKG4BY/linux-4.0-rc1---drivers--iio--accel--kxcjk-1013.ko_false-unreach-call.cil.c:6625: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-pKG4BY/linux-4.0-rc1---drivers--iio--accel--kxcjk-1013.ko_false-unreach-call.cil.c:6625: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-pKG4BY/linux-4.0-rc1---drivers--iio--accel--kxcjk-1013.ko_false-unreach-call.cil.c:6630: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-pKG4BY/linux-4.0-rc1---drivers--iio--accel--kxcjk-1013.ko_false-unreach-call.cil.c:6632: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-pKG4BY/linux-4.0-rc1---drivers--iio--accel--kxcjk-1013.ko_false-unreach-call.cil.c:6630: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-pKG4BY/linux-4.0-rc1---drivers--iio--accel--kxcjk-1013.ko_false-unreach-call.cil.c:6635: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-pKG4BY/linux-4.0-rc1---drivers--iio--accel--kxcjk-1013.ko_false-unreach-call.cil.c:8229: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-pKG4BY/linux-4.0-rc1---drivers--iio--accel--kxcjk-1013.ko_false-unreach-call.cil.c:7934: invalid function pointer
KLEE: NOTE: now ignoring this error at this location
0  klee            0x00000000012fcca8 llvm::sys::PrintStackTrace(llvm::raw_ostream&) + 56
1  klee            0x00000000012fac7e llvm::sys::RunSignalHandlers() + 62
2  klee            0x00000000012fadcc
3  libpthread.so.0 0x00007efe41e23390
4  klee            0x0000000000a59836 klee::EqExpr::create(klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&) + 38
5  klee            0x00000000005d7c3c klee::Executor::executeInstruction(klee::ExecutionState&, klee::KInstruction*) + 12060
6  klee            0x00000000005da8c5 klee::Executor::run(klee::ExecutionState&) + 2117
7  klee            0x00000000005daeef klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1391
8  klee            0x0000000000593c63 main + 8867
9  libc.so.6       0x00007efe411c7830 __libc_start_main + 240
10 klee            0x00000000005bed49 _start + 41
Running the verifier failed
RESULT: unknown
INFO: Total time elapsed: 48.305521965
