bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--media--i2c--cx25840--cx25840.ko-entry_point_true-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.: 274 172 1952 19874
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.644111871719
Defining function i2c_master_send as symbolic
Defining function i2c_transfer as symbolic
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function __kfifo_out as symbolic
Defining function printk as symbolic
Removed calls to 'v4l2_ctrl_handler_log_status' (function is undefined)
Defining function v4l2_subdev_queryctrl as symbolic
Defining function v4l2_subdev_g_ctrl as symbolic
Defining function v4l2_subdev_s_ctrl as symbolic
Defining function v4l2_subdev_g_ext_ctrls as symbolic
Defining function v4l2_subdev_s_ext_ctrls as symbolic
Defining function v4l2_subdev_try_ext_ctrls as symbolic
Defining function v4l2_subdev_querymenu as symbolic
Defining function __kfifo_in as symbolic
Removed calls to '__const_udelay' (function is undefined)
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'prepare_to_wait' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to 'destroy_workqueue' (function is undefined)
Defining function autoremove_wake_function as symbolic
Removed calls to '__wake_up' (function is undefined)
Defining function __alloc_workqueue_key as symbolic
Defining function queue_work_on as symbolic
Removed calls to 'release_firmware' (function is undefined)
Defining function request_firmware as symbolic
Removed calls to 'v4l2_i2c_subdev_init' (function is undefined)
Removed calls to 'v4l2_ctrl_handler_free' (function is undefined)
Removed calls to 'v4l2_ctrl_cluster' (function is undefined)
Removed calls to 'v4l2_device_unregister_subdev' (function is undefined)
Removed calls to '__kfifo_free' (function is undefined)
Defining function v4l2_ctrl_handler_init_class as symbolic
Defining function v4l2_ctrl_new_std as symbolic
Defining function v4l2_ctrl_handler_setup as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Defining function __kfifo_alloc as symbolic
Defining function devm_kmalloc as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'i2c_del_driver' (function is undefined)
Removed calls to 'ldv_check_final_state' (function is undefined)
Defining function i2c_register_driver as symbolic
Defining function ldv_release_1 as symbolic
Defining function ldv_probe_1 as symbolic
Defining function kmem_cache_alloc as symbolic
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  __memcpy
  __VERIFIER_assume
  __VERIFIER_calloc0
  __VERIFIER_error
  __VERIFIER_exit
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
  __VERIFIER_nondet_pointer_named
  __VERIFIER_nondet_size_t_named
  __VERIFIER_nondet_u32_named
  __VERIFIER_nondet_ulong_named
INFO: After-slicing optimizations and preparation time: 0.663999795914
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 322 129 1003 12099
INFO: Starting verification
KLEE: WARNING ONCE: function "cx23885_initialize" has inline asm
KLEE: WARNING ONCE: function "cx231xx_initialize" has inline asm
KLEE: WARNING ONCE: function "cx25840_initialize" 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_de28e22b-85da-412e-84cf-d50ba691bff4/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 7981 states (over memory cap)
KLEE: WARNING: killing 11944 states (over memory cap)
KLEE: WARNING: killing 11715 states (over memory cap)
KLEE: WARNING: killing 12023 states (over memory cap)
KLEE: WARNING: killing 11797 states (over memory cap)
KLEE: WARNING: killing 11844 states (over memory cap)
KLEE: WARNING: killing 12288 states (over memory cap)
KLEE: WARNING: killing 12332 states (over memory cap)
KLEE: WARNING: killing 6677 states (over memory cap)
KLEE: WARNING: killing 6736 states (over memory cap)
KLEE: WARNING: killing 6994 states (over memory cap)
KLEE: WARNING: killing 7188 states (over memory cap)
KLEE: WARNING: killing 7972 states (over memory cap)
KLEE: WARNING: killing 8099 states (over memory cap)
KLEE: WARNING: killing 8356 states (over memory cap)
KLEE: WARNING: killing 8875 states (over memory cap)
KLEE: WARNING: killing 9267 states (over memory cap)
KLEE: WARNING: killing 9198 states (over memory cap)
KLEE: WARNING: killing 9914 states (over memory cap)
KLEE: WARNING: killing 10626 states (over memory cap)
KLEE: WARNING: killing 11280 states (over memory cap)
KLEE: WARNING: killing 11277 states (over memory cap)
KLEE: WARNING: killing 12453 states (over memory cap)
KLEE: WARNING: killing 11923 states (over memory cap)
KLEE: WARNING: killing 12768 states (over memory cap)
KLEE: WARNING: killing 13153 states (over memory cap)
KLEE: WARNING: killing 14003 states (over memory cap)
KLEE: WARNING: killing 13801 states (over memory cap)
KLEE: WARNING: killing 14118 states (over memory cap)
KLEE: WARNING: killing 14498 states (over memory cap)
KLEE: WARNING: killing 13965 states (over memory cap)
KLEE: WARNING: killing 14217 states (over memory cap)
KLEE: WARNING: killing 14984 states (over memory cap)
KLEE: WARNING: killing 15175 states (over memory cap)
KLEE: WARNING: killing 15424 states (over memory cap)
KLEE: WARNING: killing 14887 states (over memory cap)
KLEE: WARNING: killing 15921 states (over memory cap)
KLEE: WARNING: killing 14863 states (over memory cap)
KLEE: WARNING: killing 15113 states (over memory cap)
KLEE: WARNING: killing 14899 states (over memory cap)
KLEE: WARNING: killing 15079 states (over memory cap)
KLEE: WARNING: killing 15004 states (over memory cap)
KLEE: WARNING: killing 14923 states (over memory cap)
KLEE: WARNING: killing 15361 states (over memory cap)
KLEE: WARNING: killing 14764 states (over memory cap)
KLEE: WARNING: killing 15780 states (over memory cap)
KLEE: WARNING: killing 14929 states (over memory cap)
KLEE: WARNING: killing 15173 states (over memory cap)
KLEE: WARNING: killing 15222 states (over memory cap)
KLEE: WARNING: killing 15465 states (over memory cap)
KLEE: WARNING: killing 15125 states (over memory cap)
KLEE: WARNING: killing 15690 states (over memory cap)
KLEE: WARNING: killing 15679 states (over memory cap)
KLEE: WARNING: killing 15598 states (over memory cap)
KLEE: WARNING: killing 14619 states (over memory cap)
KLEE: WARNING: killing 15888 states (over memory cap)
KLEE: WARNING: killing 15360 states (over memory cap)
KLEE: WARNING: killing 14833 states (over memory cap)
KLEE: WARNING: killing 15643 states (over memory cap)
KLEE: WARNING: killing 15183 states (over memory cap)
KLEE: WARNING: killing 15420 states (over memory cap)
KLEE: WARNING: killing 14958 states (over memory cap)
KLEE: WARNING: killing 15260 states (over memory cap)
KLEE: WARNING: killing 15185 states (over memory cap)
KLEE: WARNING: killing 15299 states (over memory cap)
KLEE: WARNING: killing 15407 states (over memory cap)
KLEE: WARNING: killing 15139 states (over memory cap)
KLEE: WARNING: killing 15063 states (over memory cap)
KLEE: WARNING: killing 14920 states (over memory cap)
KLEE: WARNING: killing 15279 states (over memory cap)
KLEE: WARNING: killing 15831 states (over memory cap)
KLEE: WARNING: killing 15192 states (over memory cap)
KLEE: WARNING: killing 15424 states (over memory cap)
KLEE: WARNING: killing 15474 states (over memory cap)
KLEE: WARNING: killing 15208 states (over memory cap)
KLEE: WARNING: killing 15324 states (over memory cap)
KLEE: WARNING: killing 15683 states (over memory cap)
KLEE: WARNING: killing 15542 states (over memory cap)
KLEE: WARNING: killing 15592 states (over memory cap)
KLEE: WARNING: killing 15887 states (over memory cap)
KLEE: WARNING: killing 15125 states (over memory cap)
KLEE: WARNING: killing 14863 states (over memory cap)
KLEE: WARNING: killing 15285 states (over memory cap)
KLEE: WARNING: killing 15270 states (over memory cap)
KLEE: WARNING: killing 15318 states (over memory cap)
KLEE: WARNING: killing 15057 states (over memory cap)
KLEE: WARNING: killing 15534 states (over memory cap)
KLEE: WARNING: killing 15215 states (over memory cap)
KLEE: WARNING: killing 15821 states (over memory cap)
KLEE: WARNING: killing 15556 states (over memory cap)
KLEE: WARNING: killing 15170 states (over memory cap)
KLEE: WARNING: killing 14661 states (over memory cap)
KLEE: WARNING: killing 15884 states (over memory cap)
KLEE: WARNING: killing 15617 states (over memory cap)
KLEE: WARNING: killing 15484 states (over memory cap)
KLEE: WARNING: killing 15351 states (over memory cap)
KLEE: WARNING: killing 15208 states (over memory cap)
KLEE: WARNING: killing 15010 states (over memory cap)
KLEE: WARNING: killing 15363 states (over memory cap)
KLEE: WARNING: killing 15164 states (over memory cap)
KLEE: WARNING: killing 15272 states (over memory cap)
KLEE: WARNING: killing 15316 states (over memory cap)
KLEE: WARNING: killing 15306 states (over memory cap)
KLEE: WARNING: killing 15474 states (over memory cap)
KLEE: WARNING: killing 15582 states (over memory cap)
KLEE: WARNING: killing 15327 states (over memory cap)
KLEE: WARNING: killing 15306 states (over memory cap)
KLEE: WARNING: killing 15176 states (over memory cap)
KLEE: WARNING: killing 15709 states (over memory cap)
KLEE: WARNING: killing 15633 states (over memory cap)
KLEE: WARNING: killing 15679 states (over memory cap)
KLEE: WARNING: killing 15601 states (over memory cap)
KLEE: WARNING: killing 15160 states (over memory cap)
KLEE: WARNING: killing 15208 states (over memory cap)
KLEE: WARNING: killing 15128 states (over memory cap)
KLEE: WARNING: killing 14994 states (over memory cap)
KLEE: WARNING: killing 15466 states (over memory cap)
KLEE: WARNING: killing 15879 states (over memory cap)
KLEE: WARNING: killing 15018 states (over memory cap)
KLEE: WARNING: killing 14940 states (over memory cap)
