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-32_7a-drivers--usb--gadget--libcomposite.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.: 334 420 3493 21650
Removed infinite loop in count_ext_compat
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.723690986633
Defining function utf8s_to_utf16s as symbolic
Defining function snprintf as symbolic
Removed calls to 'dev_err' (function is undefined)
Removed calls to '__dynamic_dev_dbg' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function usb_gadget_probe_driver as symbolic
Defining function usb_gadget_unregister_driver as symbolic
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Removed calls to 'module_put' (function is undefined)
Defining function __request_module as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Defining function try_module_get as symbolic
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'config_group_init_type_name' (function is undefined)
Defining function config_item_set_name as symbolic
Defining function sprintf as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'dev_warn' (function is undefined)
Removed calls to '_dev_info' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to 'usb_gadget_set_state' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function usb_speed_string as symbolic
Removed calls to 'device_remove_file' (function is undefined)
Defining function device_create_file as symbolic
Removed calls to 'config_item_init_type_name' (function is undefined)
Removed calls to 'config_item_put' (function is undefined)
Defining function kstrdup as symbolic
Defining function printk as symbolic
Defining function kstrtou8 as symbolic
Defining function kstrtou16 as symbolic
Defining function strtobool as symbolic
Removed calls to '__list_del_entry' (function is undefined)
Defining function usb_udc_attach_driver as symbolic
Removed calls to '__mutex_init' (function is undefined)
Defining function kmemdup as symbolic
Defining function mutex_trylock as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'configfs_unregister_subsystem' (function is undefined)
Removed calls to 'config_group_init' (function is undefined)
Defining function ldv_probe_21 as symbolic
Defining function ldv_probe_7 as symbolic
Defining function ldv_probe_26 as symbolic
Defining function ldv_probe_27 as symbolic
Defining function ldv_probe_10 as symbolic
Defining function ldv_probe_15 as symbolic
Defining function configfs_register_subsystem as symbolic
Linked our definitions to these undefined functions:
  strchr
  strcmp
  strlen
  strrchr
  __kmalloc
  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.774046897888
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 453 364 2216 13311
INFO: Starting verification
KLEE: WARNING ONCE: function "composite_setup" 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_4f3fc20b-0047-4996-bbea-467dd498ab66/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 43081 states (over memory cap)
KLEE: WARNING: killing 36770 states (over memory cap)
KLEE: WARNING: killing 35952 states (over memory cap)
KLEE: WARNING: killing 36372 states (over memory cap)
KLEE: WARNING: killing 36861 states (over memory cap)
KLEE: WARNING: killing 38202 states (over memory cap)
KLEE: WARNING: killing 39330 states (over memory cap)
KLEE: WARNING: killing 38923 states (over memory cap)
KLEE: WARNING: killing 41042 states (over memory cap)
KLEE: WARNING: killing 36924 states (over memory cap)
KLEE: WARNING: killing 39338 states (over memory cap)
KLEE: WARNING: killing 39083 states (over memory cap)
KLEE: WARNING: killing 36504 states (over memory cap)
KLEE: WARNING: killing 37708 states (over memory cap)
KLEE: WARNING: killing 38959 states (over memory cap)
KLEE: WARNING: killing 38555 states (over memory cap)
KLEE: WARNING: killing 39651 states (over memory cap)
KLEE: WARNING: killing 38261 states (over memory cap)
KLEE: WARNING: killing 37033 states (over memory cap)
KLEE: WARNING: killing 38704 states (over memory cap)
KLEE: WARNING: killing 38857 states (over memory cap)
KLEE: WARNING: killing 38901 states (over memory cap)
KLEE: WARNING: killing 38075 states (over memory cap)
KLEE: WARNING: killing 38403 states (over memory cap)
KLEE: WARNING: killing 38036 states (over memory cap)
KLEE: WARNING: killing 37927 states (over memory cap)
KLEE: WARNING: killing 38792 states (over memory cap)
KLEE: WARNING: killing 35835 states (over memory cap)
KLEE: WARNING: killing 39368 states (over memory cap)
KLEE: WARNING: killing 38684 states (over memory cap)
KLEE: WARNING: killing 38581 states (over memory cap)
KLEE: WARNING: killing 38717 states (over memory cap)
KLEE: WARNING: killing 38402 states (over memory cap)
KLEE: WARNING: killing 38177 states (over memory cap)
KLEE: WARNING: killing 37065 states (over memory cap)
KLEE: WARNING: killing 39830 states (over memory cap)
KLEE: WARNING: killing 37541 states (over memory cap)
KLEE: WARNING: killing 38240 states (over memory cap)
KLEE: WARNING: killing 39635 states (over memory cap)
KLEE: WARNING: killing 39144 states (over memory cap)
KLEE: WARNING: killing 37397 states (over memory cap)
KLEE: WARNING: killing 37929 states (over memory cap)
KLEE: WARNING: killing 39278 states (over memory cap)
KLEE: WARNING: killing 36936 states (over memory cap)
KLEE: WARNING: killing 39986 states (over memory cap)
KLEE: WARNING: killing 39139 states (over memory cap)
KLEE: WARNING: killing 38386 states (over memory cap)
KLEE: WARNING: killing 39459 states (over memory cap)
KLEE: WARNING: killing 37906 states (over memory cap)
KLEE: WARNING: killing 39749 states (over memory cap)
KLEE: WARNING: killing 36985 states (over memory cap)
KLEE: WARNING: killing 38973 states (over memory cap)
KLEE: WARNING: killing 39608 states (over memory cap)
KLEE: WARNING: killing 37812 states (over memory cap)
KLEE: WARNING: killing 37904 states (over memory cap)
KLEE: WARNING: killing 38300 states (over memory cap)
KLEE: WARNING: killing 37847 states (over memory cap)
KLEE: WARNING: killing 38978 states (over memory cap)
KLEE: WARNING: killing 37966 states (over memory cap)
KLEE: WARNING: killing 41498 states (over memory cap)
KLEE: WARNING: killing 37485 states (over memory cap)
KLEE: WARNING: killing 38013 states (over memory cap)
KLEE: WARNING: killing 38827 states (over memory cap)
KLEE: WARNING: killing 39080 states (over memory cap)
KLEE: WARNING: killing 38139 states (over memory cap)
KLEE: WARNING: killing 39201 states (over memory cap)
KLEE: WARNING: killing 39909 states (over memory cap)
KLEE: WARNING: killing 37146 states (over memory cap)
KLEE: WARNING: killing 37179 states (over memory cap)
KLEE: WARNING: killing 37856 states (over memory cap)
KLEE: WARNING: killing 40368 states (over memory cap)
KLEE: WARNING: killing 38259 states (over memory cap)
KLEE: WARNING: killing 38673 states (over memory cap)
KLEE: WARNING: killing 37042 states (over memory cap)
KLEE: WARNING: killing 40525 states (over memory cap)
KLEE: WARNING: killing 37579 states (over memory cap)
KLEE: WARNING: killing 38588 states (over memory cap)
KLEE: WARNING: killing 37735 states (over memory cap)
KLEE: WARNING: killing 38083 states (over memory cap)
KLEE: WARNING: killing 38992 states (over memory cap)
KLEE: WARNING: killing 39335 states (over memory cap)
KLEE: WARNING: killing 40848 states (over memory cap)
KLEE: WARNING: killing 38279 states (over memory cap)
KLEE: WARNING: killing 37426 states (over memory cap)
KLEE: WARNING: killing 38624 states (over memory cap)
KLEE: WARNING: killing 38891 states (over memory cap)
KLEE: WARNING: killing 37277 states (over memory cap)
KLEE: WARNING: killing 39349 states (over memory cap)
KLEE: WARNING: killing 41204 states (over memory cap)
