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-08_1a-drivers--usb--gadget--libcomposite.ko-entry_point_false-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.: 330 297 3177 20152
Removed infinite loop in count_ext_compat
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 0.702569007874
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 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function __request_module as symbolic
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
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.744215011597
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 447 239 1817 12166
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_4349d861-9d0b-4055-a57b-c20a69697aa9/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 5078 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 41377 states (over memory cap)
KLEE: WARNING: killing 34136 states (over memory cap)
KLEE: WARNING: killing 34385 states (over memory cap)
KLEE: WARNING: killing 34574 states (over memory cap)
KLEE: WARNING: killing 33840 states (over memory cap)
KLEE: WARNING: killing 37814 states (over memory cap)
KLEE: WARNING: killing 41122 states (over memory cap)
KLEE: WARNING: killing 41528 states (over memory cap)
KLEE: WARNING: killing 38407 states (over memory cap)
KLEE: WARNING: killing 38362 states (over memory cap)
KLEE: WARNING: killing 37028 states (over memory cap)
KLEE: WARNING: killing 38979 states (over memory cap)
KLEE: WARNING: killing 37179 states (over memory cap)
KLEE: WARNING: killing 39032 states (over memory cap)
KLEE: WARNING: killing 38628 states (over memory cap)
KLEE: WARNING: killing 39558 states (over memory cap)
KLEE: WARNING: killing 37432 states (over memory cap)
KLEE: WARNING: killing 36951 states (over memory cap)
KLEE: WARNING: killing 37172 states (over memory cap)
KLEE: WARNING: killing 39894 states (over memory cap)
KLEE: WARNING: killing 38800 states (over memory cap)
KLEE: WARNING: killing 39655 states (over memory cap)
KLEE: WARNING: killing 38230 states (over memory cap)
KLEE: WARNING: killing 37545 states (over memory cap)
KLEE: WARNING: killing 39550 states (over memory cap)
KLEE: WARNING: killing 37768 states (over memory cap)
KLEE: WARNING: killing 40446 states (over memory cap)
KLEE: WARNING: killing 37696 states (over memory cap)
KLEE: WARNING: killing 36532 states (over memory cap)
KLEE: WARNING: killing 38890 states (over memory cap)
KLEE: WARNING: killing 38085 states (over memory cap)
KLEE: WARNING: killing 37724 states (over memory cap)
KLEE: WARNING: killing 38488 states (over memory cap)
KLEE: WARNING: killing 37083 states (over memory cap)
KLEE: WARNING: killing 38921 states (over memory cap)
KLEE: WARNING: killing 37588 states (over memory cap)
KLEE: WARNING: killing 39343 states (over memory cap)
KLEE: WARNING: killing 35754 states (over memory cap)
KLEE: WARNING: killing 39890 states (over memory cap)
KLEE: WARNING: killing 39387 states (over memory cap)
KLEE: WARNING: killing 37127 states (over memory cap)
KLEE: WARNING: killing 38778 states (over memory cap)
KLEE: WARNING: killing 37824 states (over memory cap)
KLEE: WARNING: killing 35591 states (over memory cap)
KLEE: WARNING: killing 40771 states (over memory cap)
KLEE: WARNING: killing 39015 states (over memory cap)
KLEE: WARNING: killing 37458 states (over memory cap)
KLEE: WARNING: killing 42267 states (over memory cap)
KLEE: WARNING: killing 36975 states (over memory cap)
KLEE: WARNING: killing 37266 states (over memory cap)
KLEE: WARNING: killing 37194 states (over memory cap)
KLEE: WARNING: killing 37616 states (over memory cap)
KLEE: WARNING: killing 39466 states (over memory cap)
KLEE: WARNING: killing 37102 states (over memory cap)
KLEE: WARNING: killing 39540 states (over memory cap)
KLEE: WARNING: killing 37908 states (over memory cap)
KLEE: WARNING: killing 39728 states (over memory cap)
KLEE: WARNING: killing 38743 states (over memory cap)
KLEE: WARNING: killing 39605 states (over memory cap)
KLEE: WARNING: killing 38291 states (over memory cap)
KLEE: WARNING: killing 36079 states (over memory cap)
KLEE: WARNING: killing 39317 states (over memory cap)
KLEE: WARNING: killing 36431 states (over memory cap)
KLEE: WARNING: killing 38666 states (over memory cap)
KLEE: WARNING: killing 41052 states (over memory cap)
KLEE: WARNING: killing 36983 states (over memory cap)
KLEE: WARNING: killing 39281 states (over memory cap)
KLEE: WARNING: killing 38238 states (over memory cap)
KLEE: WARNING: killing 38204 states (over memory cap)
KLEE: WARNING: killing 39956 states (over memory cap)
KLEE: WARNING: killing 35973 states (over memory cap)
KLEE: WARNING: killing 38387 states (over memory cap)
KLEE: WARNING: killing 38458 states (over memory cap)
KLEE: WARNING: killing 37808 states (over memory cap)
KLEE: WARNING: killing 38967 states (over memory cap)
KLEE: WARNING: killing 40084 states (over memory cap)
KLEE: WARNING: killing 38662 states (over memory cap)
KLEE: WARNING: killing 38025 states (over memory cap)
KLEE: WARNING: killing 37338 states (over memory cap)
KLEE: WARNING: killing 39186 states (over memory cap)
KLEE: WARNING: killing 37276 states (over memory cap)
KLEE: WARNING: killing 40430 states (over memory cap)
KLEE: WARNING: killing 39231 states (over memory cap)
KLEE: WARNING: killing 37921 states (over memory cap)
KLEE: WARNING: killing 37465 states (over memory cap)
KLEE: WARNING: killing 37980 states (over memory cap)
KLEE: WARNING: killing 39189 states (over memory cap)
KLEE: WARNING: killing 37939 states (over memory cap)
KLEE: WARNING: killing 38319 states (over memory cap)
KLEE: WARNING: killing 38665 states (over memory cap)
KLEE: WARNING: killing 39052 states (over memory cap)
