bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.14/linux-3.14__complex_emg__linux-kernel-locking-spinlock__drivers-media-platform-marvell-ccic-cafe_ccic_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.: 184 381 1968 12159
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.506106853485
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to 'iowrite32' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function ioread32 as symbolic
Removed calls to '__ldv_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Defining function dev_err as symbolic
Defining function prepare_to_wait_event as symbolic
Defining function schedule_timeout as symbolic
Removed calls to 'pci_unregister_driver' (function is undefined)
Defining function printk as symbolic
Defining function __pci_register_driver as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'debug_dma_free_coherent' (function is undefined)
Removed calls to 'debug_dma_unmap_sg' (function is undefined)
Defining function vb2_plane_cookie as symbolic
Removed calls to 'debug_dma_alloc_coherent' (function is undefined)
Removed calls to 'debug_dma_map_sg' (function is undefined)
Defining function sg_next as symbolic
Removed calls to '__list_add' (function is undefined)
Defining function dev_warn as symbolic
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to 'msleep' (function is undefined)
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function vb2_mmap as symbolic
Defining function vb2_poll as symbolic
Defining function vb2_read as symbolic
Defining function video_ioctl2 as symbolic
Defining function vb2_dqbuf as symbolic
Defining function strlcpy as symbolic
Defining function vb2_qbuf as symbolic
Defining function vb2_querybuf as symbolic
Defining function vb2_reqbufs as symbolic
Defining function vb2_streamoff as symbolic
Defining function vb2_streamon as symbolic
Removed calls to 'ldv_check_alloc_flags' (function is undefined)
Removed calls to 'ldv_after_alloc' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'pci_set_master' (function is undefined)
Removed calls to 'i2c_del_adapter' (function is undefined)
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'pci_iounmap' (function is undefined)
Removed calls to 'pci_disable_device' (function is undefined)
Removed calls to 'pci_restore_state' (function is undefined)
Defining function pci_enable_device as symbolic
Defining function pci_save_state as symbolic
Removed calls to 'vb2_queue_release' (function is undefined)
Removed calls to 'video_unregister_device' (function is undefined)
Removed calls to 'v4l2_ctrl_handler_free' (function is undefined)
Removed calls to 'v4l2_device_unregister' (function is undefined)
Defining function pci_iomap as symbolic
Removed calls to '__mutex_init' (function is undefined)
Defining function v4l2_device_register as symbolic
Defining function v4l2_i2c_new_subdev_board as symbolic
Defining function v4l2_ctrl_handler_init_class as symbolic
Defining function __video_register_device as symbolic
Defining function i2c_add_adapter as symbolic
Defining function request_threaded_irq as symbolic
Removed calls to 'tasklet_init' (function is undefined)
Removed calls to 'vb2_dma_contig_cleanup_ctx' (function is undefined)
Defining function vb2_dma_contig_init_ctx as symbolic
Removed calls to '__tasklet_schedule' (function is undefined)
Defining function vb2_queue_init as symbolic
Defining function vb2_plane_vaddr as symbolic
Removed calls to 'vb2_buffer_done' (function is undefined)
Defining function video_devdata as symbolic
Defining function external_allocated_data as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'ldv_switch_to_interrupt_context' (function is undefined)
Removed calls to 'ldv_switch_to_process_context' (function is undefined)
Removed calls to 'ldv_pre_probe' (function is undefined)
Removed calls to 'video_device_release_empty' (function is undefined)
Removed calls to 'ldv_assert' (function is undefined)
Linked our definitions to these undefined functions:
  strcpy
  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.511140108109
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 237 311 993 6937
INFO: Starting verification
KLEE: WARNING ONCE: function "mccic_irq" has inline asm
KLEE: WARNING ONCE: function "dma_free_attrs" has inline asm
KLEE: WARNING ONCE: function "mcam_vb_sg_buf_prepare" has inline asm
KLEE: WARNING ONCE: function "mcam_vb_buf_queue" has inline asm
KLEE: WARNING ONCE: function "mcam_ctlr_dma_sg" has inline asm
KLEE: WARNING ONCE: function "mcam_read_setup" has inline asm
KLEE: WARNING ONCE: function "mcam_alloc_dma_bufs" has inline asm
KLEE: WARNING ONCE: function "mcam_vb_start_streaming" has inline asm
KLEE: WARNING ONCE: function "mcam_ctlr_stop_dma" has inline asm
KLEE: WARNING ONCE: function "mcam_vidioc_s_fmt_vid_cap" has inline asm
KLEE: WARNING ONCE: function "mccic_resume" has inline asm
KLEE: WARNING ONCE: function "mccic_register" has inline asm
KLEE: WARNING ONCE: function "mcam_v4l_open" has inline asm
KLEE: WARNING ONCE: function "mcam_dma_sg_done" has inline asm
KLEE: WARNING ONCE: function "mcam_set_contig_buffer" has inline asm
KLEE: WARNING: undefined reference to function: video_device_release_empty
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_b84ccd38-13f7-4adb-a0b2-9273f2e8a63e/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 17059 states (over memory cap)
KLEE: WARNING: killing 16281 states (over memory cap)
KLEE: WARNING: killing 16573 states (over memory cap)
KLEE: WARNING: killing 16633 states (over memory cap)
KLEE: WARNING: killing 15865 states (over memory cap)
KLEE: WARNING: killing 16395 states (over memory cap)
KLEE: WARNING: killing 15745 states (over memory cap)
KLEE: WARNING: killing 16037 states (over memory cap)
KLEE: WARNING: killing 16223 states (over memory cap)
KLEE: WARNING: killing 15931 states (over memory cap)
KLEE: WARNING: killing 16003 states (over memory cap)
KLEE: WARNING: killing 16531 states (over memory cap)
KLEE: WARNING: killing 17055 states (over memory cap)
KLEE: WARNING: killing 16891 states (over memory cap)
KLEE: WARNING: killing 17415 states (over memory cap)
KLEE: WARNING: killing 17478 states (over memory cap)
KLEE: WARNING: killing 17891 states (over memory cap)
KLEE: WARNING: killing 16582 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-Dw4KqU/linux-3.14__complex_emg__linux-kernel-locking-spinlock__drivers-media-platform-marvell-ccic-cafe_ccic_true-unreach-call.cil.c:10282: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 17438 states (over memory cap)
KLEE: WARNING: killing 17064 states (over memory cap)
KLEE: WARNING: killing 16905 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-Dw4KqU/linux-3.14__complex_emg__linux-kernel-locking-spinlock__drivers-media-platform-marvell-ccic-cafe_ccic_true-unreach-call.cil.c:11753: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 17312 states (over memory cap)
KLEE: WARNING: killing 16939 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-Dw4KqU/linux-3.14__complex_emg__linux-kernel-locking-spinlock__drivers-media-platform-marvell-ccic-cafe_ccic_true-unreach-call.cil.c:10237: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 17127 states (over memory cap)
KLEE: WARNING: killing 16634 states (over memory cap)
KLEE: WARNING: killing 16595 states (over memory cap)
KLEE: WARNING: killing 16554 states (over memory cap)
KLEE: WARNING: killing 16504 states (over memory cap)
KLEE: WARNING: killing 16022 states (over memory cap)
KLEE: WARNING: killing 15878 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-Dw4KqU/linux-3.14__complex_emg__linux-kernel-locking-spinlock__drivers-media-platform-marvell-ccic-cafe_ccic_true-unreach-call.cil.c:10316: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 15955 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-Dw4KqU/linux-3.14__complex_emg__linux-kernel-locking-spinlock__drivers-media-platform-marvell-ccic-cafe_ccic_true-unreach-call.cil.c:10097: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16577 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-Dw4KqU/linux-3.14__complex_emg__linux-kernel-locking-spinlock__drivers-media-platform-marvell-ccic-cafe_ccic_true-unreach-call.cil.c:10185: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16761 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-Dw4KqU/linux-3.14__complex_emg__linux-kernel-locking-spinlock__drivers-media-platform-marvell-ccic-cafe_ccic_true-unreach-call.cil.c:10359: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16399 states (over memory cap)
KLEE: WARNING: killing 16468 states (over memory cap)
KLEE: WARNING: killing 16758 states (over memory cap)
KLEE: WARNING: killing 16830 states (over memory cap)
KLEE: WARNING: killing 16470 states (over memory cap)
KLEE: WARNING: killing 16864 states (over memory cap)
KLEE: WARNING: killing 16395 states (over memory cap)
KLEE: WARNING: killing 16364 states (over memory cap)
KLEE: WARNING: killing 16323 states (over memory cap)
KLEE: WARNING: killing 16509 states (over memory cap)
KLEE: WARNING: killing 16041 states (over memory cap)
KLEE: WARNING: killing 16335 states (over memory cap)
KLEE: WARNING: killing 16626 states (over memory cap)
KLEE: WARNING: killing 16592 states (over memory cap)
KLEE: WARNING: killing 16018 states (over memory cap)
KLEE: WARNING: killing 16205 states (over memory cap)
KLEE: WARNING: killing 16267 states (over memory cap)
KLEE: WARNING: killing 16668 states (over memory cap)
KLEE: WARNING: killing 16532 states (over memory cap)
KLEE: WARNING: killing 16397 states (over memory cap)
KLEE: WARNING: killing 16887 states (over memory cap)
KLEE: WARNING: killing 16857 states (over memory cap)
KLEE: WARNING: killing 16936 states (over memory cap)
KLEE: WARNING: killing 16795 states (over memory cap)
KLEE: WARNING: killing 16344 states (over memory cap)
KLEE: WARNING: killing 15988 states (over memory cap)
KLEE: WARNING: killing 15857 states (over memory cap)
KLEE: WARNING: killing 16029 states (over memory cap)
KLEE: WARNING: killing 16324 states (over memory cap)
KLEE: WARNING: killing 16602 states (over memory cap)
KLEE: WARNING: killing 16259 states (over memory cap)
KLEE: WARNING: killing 16955 states (over memory cap)
KLEE: WARNING: killing 16310 states (over memory cap)
KLEE: WARNING: killing 16269 states (over memory cap)
KLEE: WARNING: killing 16132 states (over memory cap)
KLEE: WARNING: killing 16211 states (over memory cap)
KLEE: WARNING: killing 16482 states (over memory cap)
KLEE: WARNING: killing 16149 states (over memory cap)
KLEE: WARNING: killing 16734 states (over memory cap)
KLEE: WARNING: killing 16493 states (over memory cap)
KLEE: WARNING: killing 16674 states (over memory cap)
KLEE: WARNING: killing 16341 states (over memory cap)
KLEE: WARNING: killing 16300 states (over memory cap)
KLEE: WARNING: killing 16378 states (over memory cap)
KLEE: WARNING: killing 16347 states (over memory cap)
KLEE: WARNING: killing 16317 states (over memory cap)
KLEE: WARNING: killing 16691 states (over memory cap)
KLEE: WARNING: killing 16366 states (over memory cap)
KLEE: WARNING: killing 16434 states (over memory cap)
KLEE: WARNING: killing 15997 states (over memory cap)
KLEE: WARNING: killing 16367 states (over memory cap)
KLEE: WARNING: killing 15945 states (over memory cap)
KLEE: WARNING: killing 16407 states (over memory cap)
KLEE: WARNING: killing 16481 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-Dw4KqU/linux-3.14__complex_emg__linux-kernel-locking-spinlock__drivers-media-platform-marvell-ccic-cafe_ccic_true-unreach-call.cil.c:10981: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16550 states (over memory cap)
KLEE: WARNING: killing 16014 states (over memory cap)
KLEE: WARNING: killing 16281 states (over memory cap)
