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--iio--accel--kxcjk-1013.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.: 153 125 1256 6040
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 0.270378112793
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)
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (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_trigger_register 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 find_first_bit as symbolic
Defining function find_next_bit as symbolic
Defining function iio_push_to_buffers as symbolic
Defining function i2c_smbus_read_word_data 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_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 __pm_runtime_suspend as symbolic
Defining function __pm_runtime_resume as symbolic
Defining function iio_read_const_attr as symbolic
Defining function iio_triggered_buffer_postenable as symbolic
Defining function iio_triggered_buffer_predisable as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'i2c_del_driver' (function is undefined)
Defining function ldv_suspend_late_6 as symbolic
Defining function ldv_restore_early_6 as symbolic
Defining function ldv_resume_early_6 as symbolic
Defining function ldv_thaw_early_6 as symbolic
Defining function ldv_resume_noirq_6 as symbolic
Defining function ldv_freeze_noirq_6 as symbolic
Defining function ldv_prepare_6 as symbolic
Defining function ldv_freeze_late_6 as symbolic
Defining function ldv_thaw_noirq_6 as symbolic
Defining function ldv_poweroff_noirq_6 as symbolic
Defining function ldv_poweroff_late_6 as symbolic
Defining function ldv_restore_noirq_6 as symbolic
Defining function ldv_suspend_noirq_6 as symbolic
Defining function ldv_complete_6 as symbolic
Defining function ldv_release_8 as symbolic
Defining function ldv_probe_8 as symbolic
Defining function i2c_register_driver as symbolic
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.283524036407
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 203 129 711 3289
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_bc9e540d-2413-45c1-80ca-85d089d85f46/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-PJT4Fp/linux-4.2-rc1.tar.xz-08_1a-drivers--iio--accel--kxcjk-1013.ko-entry_point_false-unreach-call.cil.out.c:5500: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-PJT4Fp/linux-4.2-rc1.tar.xz-08_1a-drivers--iio--accel--kxcjk-1013.ko-entry_point_false-unreach-call.cil.out.c:5524: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-PJT4Fp/linux-4.2-rc1.tar.xz-08_1a-drivers--iio--accel--kxcjk-1013.ko-entry_point_false-unreach-call.cil.out.c:5978: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-PJT4Fp/linux-4.2-rc1.tar.xz-08_1a-drivers--iio--accel--kxcjk-1013.ko-entry_point_false-unreach-call.cil.out.c:5759: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-PJT4Fp/linux-4.2-rc1.tar.xz-08_1a-drivers--iio--accel--kxcjk-1013.ko-entry_point_false-unreach-call.cil.out.c:5759: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-PJT4Fp/linux-4.2-rc1.tar.xz-08_1a-drivers--iio--accel--kxcjk-1013.ko-entry_point_false-unreach-call.cil.out.c:5765: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-PJT4Fp/linux-4.2-rc1.tar.xz-08_1a-drivers--iio--accel--kxcjk-1013.ko-entry_point_false-unreach-call.cil.out.c:5768: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-PJT4Fp/linux-4.2-rc1.tar.xz-08_1a-drivers--iio--accel--kxcjk-1013.ko-entry_point_false-unreach-call.cil.out.c:4774: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-PJT4Fp/linux-4.2-rc1.tar.xz-08_1a-drivers--iio--accel--kxcjk-1013.ko-entry_point_false-unreach-call.cil.out.c:5763: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 12374 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: ERROR: /tmp/symbiotic-PJT4Fp/linux-4.2-rc1.tar.xz-08_1a-drivers--iio--accel--kxcjk-1013.ko-entry_point_false-unreach-call.cil.out.c:5786: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 13087 states (over memory cap)
KLEE: WARNING: killing 13516 states (over memory cap)
KLEE: WARNING: killing 13026 states (over memory cap)
KLEE: WARNING: killing 12718 states (over memory cap)
KLEE: WARNING: killing 12683 states (over memory cap)
KLEE: WARNING: killing 12287 states (over memory cap)
KLEE: WARNING: killing 12618 states (over memory cap)
KLEE: WARNING: killing 13304 states (over memory cap)
KLEE: WARNING: killing 12910 states (over memory cap)
KLEE: WARNING: killing 12967 states (over memory cap)
KLEE: WARNING: killing 13286 states (over memory cap)
KLEE: WARNING: killing 13616 states (over memory cap)
KLEE: WARNING: killing 13399 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-PJT4Fp/linux-4.2-rc1.tar.xz-08_1a-drivers--iio--accel--kxcjk-1013.ko-entry_point_false-unreach-call.cil.out.c:4647: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 13894 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-PJT4Fp/linux-4.2-rc1.tar.xz-08_1a-drivers--iio--accel--kxcjk-1013.ko-entry_point_false-unreach-call.cil.out.c:5935: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 13329 states (over memory cap)
KLEE: WARNING: killing 13478 states (over memory cap)
KLEE: WARNING: killing 13804 states (over memory cap)
KLEE: WARNING: killing 13784 states (over memory cap)
KLEE: WARNING: killing 14027 states (over memory cap)
KLEE: WARNING: killing 14273 states (over memory cap)
KLEE: WARNING: killing 14077 states (over memory cap)
KLEE: WARNING: killing 13790 states (over memory cap)
KLEE: WARNING: killing 14122 states (over memory cap)
KLEE: WARNING: killing 14016 states (over memory cap)
KLEE: WARNING: killing 13733 states (over memory cap)
KLEE: WARNING: killing 14065 states (over memory cap)
KLEE: WARNING: killing 13693 states (over memory cap)
KLEE: WARNING: killing 13848 states (over memory cap)
KLEE: WARNING: killing 14089 states (over memory cap)
KLEE: WARNING: killing 13280 states (over memory cap)
KLEE: WARNING: killing 13697 states (over memory cap)
KLEE: WARNING: killing 12978 states (over memory cap)
KLEE: WARNING: killing 13043 states (over memory cap)
KLEE: WARNING: killing 13373 states (over memory cap)
KLEE: WARNING: killing 13527 states (over memory cap)
KLEE: WARNING: killing 13074 states (over memory cap)
KLEE: WARNING: killing 13396 states (over memory cap)
KLEE: WARNING: killing 13039 states (over memory cap)
KLEE: WARNING: killing 13276 states (over memory cap)
KLEE: WARNING: killing 12995 states (over memory cap)
KLEE: WARNING: killing 13063 states (over memory cap)
KLEE: WARNING: killing 13043 states (over memory cap)
KLEE: WARNING: killing 13115 states (over memory cap)
KLEE: WARNING: killing 13435 states (over memory cap)
KLEE: WARNING: killing 13083 states (over memory cap)
KLEE: WARNING: killing 12977 states (over memory cap)
KLEE: WARNING: killing 13216 states (over memory cap)
KLEE: WARNING: killing 13540 states (over memory cap)
KLEE: WARNING: killing 13099 states (over memory cap)
KLEE: WARNING: killing 13331 states (over memory cap)
KLEE: WARNING: killing 13398 states (over memory cap)
KLEE: WARNING: killing 12711 states (over memory cap)
KLEE: WARNING: killing 13537 states (over memory cap)
KLEE: WARNING: killing 13692 states (over memory cap)
KLEE: WARNING: killing 13002 states (over memory cap)
KLEE: WARNING: killing 13663 states (over memory cap)
KLEE: WARNING: killing 13566 states (over memory cap)
KLEE: WARNING: killing 13466 states (over memory cap)
KLEE: WARNING: killing 14039 states (over memory cap)
KLEE: WARNING: killing 14018 states (over memory cap)
KLEE: WARNING: killing 13332 states (over memory cap)
KLEE: WARNING: killing 13323 states (over memory cap)
KLEE: WARNING: killing 13561 states (over memory cap)
KLEE: WARNING: killing 13542 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-PJT4Fp/linux-4.2-rc1.tar.xz-08_1a-drivers--iio--accel--kxcjk-1013.ko-entry_point_false-unreach-call.cil.out.c:5339: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 13275 states (over memory cap)
KLEE: WARNING: killing 13011 states (over memory cap)
KLEE: WARNING: killing 13078 states (over memory cap)
KLEE: WARNING: killing 13144 states (over memory cap)
KLEE: WARNING: killing 13048 states (over memory cap)
KLEE: WARNING: killing 13945 states (over memory cap)
KLEE: WARNING: killing 13264 states (over memory cap)
KLEE: WARNING: killing 12747 states (over memory cap)
KLEE: WARNING: killing 13642 states (over memory cap)
KLEE: WARNING: killing 13128 states (over memory cap)
KLEE: WARNING: killing 13365 states (over memory cap)
KLEE: WARNING: killing 13763 states (over memory cap)
KLEE: WARNING: killing 13174 states (over memory cap)
KLEE: WARNING: killing 13823 states (over memory cap)
KLEE: WARNING: killing 13725 states (over memory cap)
KLEE: WARNING: killing 13050 states (over memory cap)
KLEE: WARNING: killing 13035 states (over memory cap)
KLEE: WARNING: killing 13264 states (over memory cap)
KLEE: WARNING: killing 13423 states (over memory cap)
KLEE: WARNING: killing 13000 states (over memory cap)
KLEE: WARNING: killing 13392 states (over memory cap)
KLEE: WARNING: killing 13459 states (over memory cap)
KLEE: WARNING: killing 14020 states (over memory cap)
KLEE: WARNING: killing 13267 states (over memory cap)
KLEE: WARNING: killing 13584 states (over memory cap)
KLEE: WARNING: killing 12747 states (over memory cap)
KLEE: WARNING: killing 12650 states (over memory cap)
KLEE: WARNING: killing 12717 states (over memory cap)
KLEE: WARNING: killing 12785 states (over memory cap)
KLEE: WARNING: killing 13738 states (over memory cap)
KLEE: WARNING: killing 13571 states (over memory cap)
KLEE: WARNING: killing 13393 states (over memory cap)
KLEE: WARNING: killing 14110 states (over memory cap)
KLEE: WARNING: killing 13448 states (over memory cap)
KLEE: WARNING: killing 13269 states (over memory cap)
KLEE: WARNING: killing 13181 states (over memory cap)
KLEE: WARNING: killing 13809 states (over memory cap)
KLEE: WARNING: killing 13157 states (over memory cap)
KLEE: WARNING: killing 13382 states (over memory cap)
KLEE: WARNING: killing 12974 states (over memory cap)
KLEE: WARNING: killing 12956 states (over memory cap)
KLEE: WARNING: killing 13104 states (over memory cap)
KLEE: WARNING: killing 13808 states (over memory cap)
KLEE: WARNING: killing 13800 states (over memory cap)
KLEE: WARNING: killing 13387 states (over memory cap)
KLEE: WARNING: killing 13294 states (over memory cap)
KLEE: WARNING: killing 13997 states (over memory cap)
KLEE: WARNING: killing 12945 states (over memory cap)
KLEE: WARNING: killing 13567 states (over memory cap)
KLEE: WARNING: killing 12837 states (over memory cap)
KLEE: WARNING: killing 13136 states (over memory cap)
KLEE: WARNING: killing 13441 states (over memory cap)
KLEE: WARNING: killing 13193 states (over memory cap)
KLEE: WARNING: killing 13889 states (over memory cap)
KLEE: WARNING: killing 13245 states (over memory cap)
KLEE: WARNING: killing 12993 states (over memory cap)
KLEE: WARNING: killing 13217 states (over memory cap)
KLEE: WARNING: killing 12332 states (over memory cap)
KLEE: WARNING: killing 13428 states (over memory cap)
KLEE: WARNING: killing 12938 states (over memory cap)
KLEE: WARNING: killing 13636 states (over memory cap)
KLEE: WARNING: killing 13940 states (over memory cap)
KLEE: WARNING: killing 13535 states (over memory cap)
KLEE: WARNING: killing 13606 states (over memory cap)
