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--usb--pwc--pwc.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.: 230 147 1779 11860
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.503577947617
Defining function vb2_ioctl_reqbufs as symbolic
Defining function vb2_ioctl_querybuf as symbolic
Defining function vb2_ioctl_qbuf as symbolic
Defining function vb2_ioctl_dqbuf as symbolic
Defining function vb2_ioctl_streamon as symbolic
Defining function vb2_ioctl_streamoff as symbolic
Defining function v4l2_ctrl_log_status as symbolic
Defining function v4l2_ctrl_subscribe_event as symbolic
Defining function v4l2_event_unsubscribe as symbolic
Defining function video_devdata as symbolic
Removed calls to 'usb_kill_urb' (function is undefined)
Removed calls to 'usb_free_coherent' (function is undefined)
Removed calls to 'usb_free_urb' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to 'vb2_buffer_done' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function printk as symbolic
Defining function usb_set_interface as symbolic
Defining function usb_control_msg as symbolic
Defining function mutex_lock_interruptible_nested as symbolic
Defining function usb_ifnum_to_if as symbolic
Defining function usb_altnum_to_altsetting as symbolic
Defining function usb_submit_urb as symbolic
Defining function usb_alloc_coherent as symbolic
Defining function usb_alloc_urb as symbolic
Removed calls to '__mutex_init' (function is undefined)
Defining function vb2_plane_vaddr as symbolic
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function vzalloc as symbolic
Defining function vb2_fop_read as symbolic
Defining function vb2_fop_poll as symbolic
Defining function video_ioctl2 as symbolic
Defining function vb2_fop_mmap as symbolic
Defining function v4l2_fh_open as symbolic
Defining function vb2_fop_release as symbolic
Removed calls to 'v4l2_device_disconnect' (function is undefined)
Removed calls to 'video_unregister_device' (function is undefined)
Removed calls to 'input_unregister_device' (function is undefined)
Defining function v4l2_device_put as symbolic
Defining function usb_string as symbolic
Removed calls to 'v4l2_ctrl_auto_cluster' (function is undefined)
Removed calls to 'v4l2_ctrl_cluster' (function is undefined)
Defining function snprintf as symbolic
Defining function v4l2_ctrl_handler_init_class as symbolic
Defining function v4l2_ctrl_new_std as symbolic
Defining function v4l2_ctrl_get_name as symbolic
Defining function v4l2_ctrl_new_custom as symbolic
Defining function v4l2_ctrl_new_std_menu as symbolic
Defining function strlcpy as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'video_device_release_empty' (function is undefined)
Removed calls to 'usb_deregister' (function is undefined)
Removed calls to 'vb2_ops_wait_prepare' (function is undefined)
Removed calls to 'vb2_ops_wait_finish' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to 'vfree' (function is undefined)
Removed calls to 'ldv_check_final_state' (function is undefined)
Defining function ldv_probe_4 as symbolic
Defining function usb_register_driver as symbolic
Defining function kmem_cache_alloc as symbolic
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  strcpy
  __kmalloc
  __memcpy
  kfree
  __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_uint_named
  __VERIFIER_nondet_ulong_named
INFO: After-slicing optimizations and preparation time: 0.485970973969
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 229 137 903 6049
INFO: Starting verification
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_79257084-5e9b-4c8c-88a1-200de967f5ab/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 12948 states (over memory cap)
KLEE: WARNING: killing 11979 states (over memory cap)
KLEE: WARNING: killing 11722 states (over memory cap)
KLEE: WARNING: killing 11772 states (over memory cap)
KLEE: WARNING: killing 11437 states (over memory cap)
KLEE: WARNING: killing 11723 states (over memory cap)
KLEE: WARNING: killing 11079 states (over memory cap)
KLEE: WARNING: killing 11289 states (over memory cap)
KLEE: WARNING: killing 11262 states (over memory cap)
KLEE: WARNING: killing 11012 states (over memory cap)
KLEE: WARNING: killing 11374 states (over memory cap)
KLEE: WARNING: killing 11585 states (over memory cap)
KLEE: WARNING: killing 11489 states (over memory cap)
KLEE: WARNING: killing 12387 states (over memory cap)
KLEE: WARNING: killing 12064 states (over memory cap)
KLEE: WARNING: killing 12433 states (over memory cap)
KLEE: WARNING: killing 11575 states (over memory cap)
KLEE: WARNING: killing 11786 states (over memory cap)
KLEE: WARNING: killing 11470 states (over memory cap)
KLEE: WARNING: killing 11757 states (over memory cap)
KLEE: WARNING: killing 12269 states (over memory cap)
KLEE: WARNING: killing 11348 states (over memory cap)
KLEE: WARNING: killing 11711 states (over memory cap)
KLEE: WARNING: killing 11469 states (over memory cap)
KLEE: WARNING: killing 11900 states (over memory cap)
KLEE: WARNING: killing 11660 states (over memory cap)
KLEE: WARNING: killing 11870 states (over memory cap)
KLEE: WARNING: killing 11708 states (over memory cap)
KLEE: WARNING: killing 11395 states (over memory cap)
KLEE: WARNING: killing 11750 states (over memory cap)
KLEE: WARNING: killing 11364 states (over memory cap)
KLEE: WARNING: killing 11720 states (over memory cap)
KLEE: WARNING: killing 11858 states (over memory cap)
KLEE: WARNING: killing 11763 states (over memory cap)
KLEE: WARNING: killing 11676 states (over memory cap)
KLEE: WARNING: killing 11883 states (over memory cap)
KLEE: WARNING: killing 11425 states (over memory cap)
KLEE: WARNING: killing 12083 states (over memory cap)
KLEE: WARNING: killing 11770 states (over memory cap)
KLEE: WARNING: killing 11759 states (over memory cap)
KLEE: WARNING: killing 11523 states (over memory cap)
KLEE: WARNING: killing 11359 states (over memory cap)
KLEE: WARNING: killing 11787 states (over memory cap)
KLEE: WARNING: killing 11403 states (over memory cap)
KLEE: WARNING: killing 11391 states (over memory cap)
KLEE: WARNING: killing 11228 states (over memory cap)
KLEE: WARNING: killing 11359 states (over memory cap)
KLEE: WARNING: killing 11641 states (over memory cap)
KLEE: WARNING: killing 11334 states (over memory cap)
KLEE: WARNING: killing 11682 states (over memory cap)
KLEE: WARNING: killing 11742 states (over memory cap)
KLEE: WARNING: killing 11730 states (over memory cap)
KLEE: WARNING: killing 11422 states (over memory cap)
KLEE: WARNING: killing 11699 states (over memory cap)
KLEE: WARNING: killing 11613 states (over memory cap)
KLEE: WARNING: killing 11599 states (over memory cap)
KLEE: WARNING: killing 12091 states (over memory cap)
KLEE: WARNING: killing 11570 states (over memory cap)
KLEE: WARNING: killing 11267 states (over memory cap)
KLEE: WARNING: killing 11981 states (over memory cap)
KLEE: WARNING: killing 12109 states (over memory cap)
KLEE: WARNING: killing 12096 states (over memory cap)
KLEE: WARNING: killing 11579 states (over memory cap)
KLEE: WARNING: killing 11275 states (over memory cap)
KLEE: WARNING: killing 11474 states (over memory cap)
KLEE: WARNING: killing 11460 states (over memory cap)
KLEE: WARNING: killing 11879 states (over memory cap)
KLEE: WARNING: killing 11793 states (over memory cap)
KLEE: WARNING: killing 11352 states (over memory cap)
KLEE: WARNING: killing 11191 states (over memory cap)
KLEE: WARNING: killing 11321 states (over memory cap)
KLEE: WARNING: killing 11736 states (over memory cap)
KLEE: WARNING: killing 11580 states (over memory cap)
KLEE: WARNING: killing 11498 states (over memory cap)
KLEE: WARNING: killing 11771 states (over memory cap)
KLEE: WARNING: killing 11898 states (over memory cap)
KLEE: WARNING: killing 11745 states (over memory cap)
KLEE: WARNING: killing 11592 states (over memory cap)
KLEE: WARNING: killing 11577 states (over memory cap)
KLEE: WARNING: killing 11284 states (over memory cap)
KLEE: WARNING: killing 11486 states (over memory cap)
KLEE: WARNING: killing 11324 states (over memory cap)
KLEE: WARNING: killing 11808 states (over memory cap)
KLEE: WARNING: killing 12150 states (over memory cap)
KLEE: WARNING: killing 11644 states (over memory cap)
KLEE: WARNING: killing 11699 states (over memory cap)
KLEE: WARNING: killing 11690 states (over memory cap)
KLEE: WARNING: killing 11678 states (over memory cap)
KLEE: WARNING: killing 11731 states (over memory cap)
KLEE: WARNING: killing 11654 states (over memory cap)
KLEE: WARNING: killing 11432 states (over memory cap)
KLEE: WARNING: killing 11557 states (over memory cap)
KLEE: WARNING: killing 11128 states (over memory cap)
KLEE: WARNING: killing 11530 states (over memory cap)
KLEE: WARNING: killing 11941 states (over memory cap)
KLEE: WARNING: killing 11304 states (over memory cap)
KLEE: WARNING: killing 11850 states (over memory cap)
KLEE: WARNING: killing 12046 states (over memory cap)
KLEE: WARNING: killing 11763 states (over memory cap)
KLEE: WARNING: killing 11754 states (over memory cap)
KLEE: WARNING: killing 11531 states (over memory cap)
KLEE: WARNING: killing 11658 states (over memory cap)
KLEE: WARNING: killing 11509 states (over memory cap)
KLEE: WARNING: killing 11774 states (over memory cap)
KLEE: WARNING: killing 11625 states (over memory cap)
KLEE: WARNING: killing 11408 states (over memory cap)
KLEE: WARNING: killing 11463 states (over memory cap)
KLEE: WARNING: killing 11110 states (over memory cap)
KLEE: WARNING: killing 11857 states (over memory cap)
KLEE: WARNING: killing 11638 states (over memory cap)
KLEE: WARNING: killing 11696 states (over memory cap)
KLEE: WARNING: killing 11409 states (over memory cap)
KLEE: WARNING: killing 11331 states (over memory cap)
KLEE: WARNING: killing 11800 states (over memory cap)
KLEE: WARNING: killing 11315 states (over memory cap)
KLEE: WARNING: killing 11921 states (over memory cap)
KLEE: WARNING: killing 12113 states (over memory cap)
KLEE: WARNING: killing 11967 states (over memory cap)
KLEE: WARNING: killing 11614 states (over memory cap)
KLEE: WARNING: killing 11876 states (over memory cap)
KLEE: WARNING: killing 11529 states (over memory cap)
KLEE: WARNING: killing 11721 states (over memory cap)
KLEE: WARNING: killing 10964 states (over memory cap)
KLEE: WARNING: killing 11703 states (over memory cap)
KLEE: WARNING: killing 11346 states (over memory cap)
KLEE: WARNING: killing 11742 states (over memory cap)
KLEE: WARNING: killing 11390 states (over memory cap)
KLEE: WARNING: killing 11718 states (over memory cap)
KLEE: WARNING: killing 11373 states (over memory cap)
KLEE: WARNING: killing 11631 states (over memory cap)
KLEE: WARNING: killing 11487 states (over memory cap)
KLEE: WARNING: killing 11546 states (over memory cap)
KLEE: WARNING: killing 11327 states (over memory cap)
KLEE: WARNING: killing 11724 states (over memory cap)
KLEE: WARNING: killing 11850 states (over memory cap)
KLEE: WARNING: killing 11504 states (over memory cap)
KLEE: WARNING: killing 11287 states (over memory cap)
KLEE: WARNING: killing 11411 states (over memory cap)
KLEE: WARNING: killing 11672 states (over memory cap)
KLEE: WARNING: killing 11730 states (over memory cap)
KLEE: WARNING: killing 11917 states (over memory cap)
KLEE: WARNING: killing 11844 states (over memory cap)
KLEE: WARNING: killing 11568 states (over memory cap)
KLEE: WARNING: killing 11087 states (over memory cap)
KLEE: WARNING: killing 11278 states (over memory cap)
KLEE: WARNING: killing 11331 states (over memory cap)
KLEE: WARNING: killing 11392 states (over memory cap)
KLEE: WARNING: killing 11910 states (over memory cap)
KLEE: WARNING: killing 11905 states (over memory cap)
KLEE: WARNING: killing 11363 states (over memory cap)
KLEE: WARNING: killing 11881 states (over memory cap)
KLEE: WARNING: killing 12073 states (over memory cap)
KLEE: WARNING: killing 11930 states (over memory cap)
KLEE: WARNING: killing 11794 states (over memory cap)
KLEE: WARNING: killing 11652 states (over memory cap)
KLEE: WARNING: killing 11181 states (over memory cap)
KLEE: WARNING: killing 11565 states (over memory cap)
