bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i


--------------------------------------------------------------------------------


5.0.0-KLEE:86e6f6f8-dg:03407af1-symbiotic:a8aa8ad6-minisat:3db58943-stp:17249213-sbt-instrumentation:dd7e4312
INFO: After compilation stats: Globals/Functions/Blocks/Instr.: 60 52 684 3830
Removed infinite loop in ldv_assume_stop
INFO: Compilation, preparation and instrumentation time: 0.243825912476
Defining function printk as symbolic
Defining function parport_register_driver as symbolic
Removed calls to '__mutex_init' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Removed calls to 'parport_release' (function is undefined)
Removed calls to 'parport_unregister_device' (function is undefined)
Defining function parport_claim_or_block as symbolic
Defining function __video_register_device as symbolic
Defining function msecs_to_jiffies as symbolic
Defining function msleep_interruptible as symbolic
Defining function strlcpy as symbolic
Defining function v4l2_device_register as symbolic
Defining function parport_register_device as symbolic
Defining function dev_set_drvdata as symbolic
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'might_fault' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function video_ioctl2 as symbolic
Defining function copy_user_generic_unrolled as symbolic
Defining function copy_user_generic_string as symbolic
Defining function _cond_resched as symbolic
Defining function video_devdata as symbolic
Defining function dev_get_drvdata as symbolic
Defining function v4l2_ctrl_query_fill as symbolic
Removed calls to 'video_unregister_device' (function is undefined)
Removed calls to 'parport_unregister_driver' (function is undefined)
Removed calls to 'ldv_initialize' (function is undefined)
Defining function ldv_undefined_pointer as symbolic
Linked our definitions to these undefined functions:
  strcmp
  __kmalloc
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 0.196503162384
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 117 58 308 2090
INFO: Starting verification
KLEE: WARNING ONCE: function "qcam_read" has inline asm
KLEE: WARNING: undefined reference to function: video_device_release_empty
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6521: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6235: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6255: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6255: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6429: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6542: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6520: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6225: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6225: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6277: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6226: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6413: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6319: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6242: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6413: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6413: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6414: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:5879: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6433: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6361: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6414: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6415: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6337: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6815: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6431: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6416: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6334: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6417: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6379: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6373: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6337: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6331: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:4625: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6331: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6334: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6448: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6379: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6379: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6376: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6418: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6376: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6376: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6449: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6390: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6419: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6450: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6373: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6373: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6451: memory error: out of bound pointer
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: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6452: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6740: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:5628: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:6430: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:5628: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-AWCKzt/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i.pp.i:5628: invalid function pointer
KLEE: NOTE: now ignoring this error at this location
