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-43_2a-drivers--staging--unisys--visorbus--visorbus.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.: 364 332 2488 15489
Removed infinite loop in __cpuid
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.789897918701
Defining function add_uevent_var as symbolic
Removed calls to 'down' (function is undefined)
Removed calls to 'up' (function is undefined)
Removed calls to 'put_device' (function is undefined)
Defining function driver_register as symbolic
Defining function driver_create_file as symbolic
Defining function snprintf as symbolic
Defining function kobject_uevent as symbolic
Removed calls to '_raw_write_lock' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to '_raw_write_unlock' (function is undefined)
Defining function schedule_timeout_interruptible as symbolic
Defining function __msecs_to_jiffies as symbolic
Defining function cancel_delayed_work as symbolic
Defining function get_device as symbolic
Defining function bus_find_device as symbolic
Removed calls to 'driver_remove_file' (function is undefined)
Removed calls to 'driver_unregister' (function is undefined)
Removed calls to 'free_pages' (function is undefined)
Defining function kobject_init_and_add as symbolic
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to 'init_timer_key' (function is undefined)
Defining function queue_delayed_work_on as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to '__release_region' (function is undefined)
Removed calls to 'iounmap' (function is undefined)
Defining function __request_region as symbolic
Defining function ioremap_cache as symbolic
Defining function sprintf as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function seq_printf as symbolic
Defining function seq_puts as symbolic
Removed calls to '__rwlock_init' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to 'device_initialize' (function is undefined)
Removed calls to 'device_unregister' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to 'kobject_del' (function is undefined)
Removed calls to 'kobject_put' (function is undefined)
Defining function dev_set_name as symbolic
Defining function device_add as symbolic
Defining function device_register as symbolic
Defining function printk as symbolic
Defining function kstrtou8 as symbolic
Defining function scnprintf as symbolic
Defining function kstrtoint as symbolic
Defining function kstrtouint as symbolic
Defining function kstrtou16 as symbolic
Defining function sscanf as symbolic
Removed calls to 'cdev_init' (function is undefined)
Removed calls to 'unregister_chrdev_region' (function is undefined)
Removed calls to 'flush_workqueue' (function is undefined)
Removed calls to 'destroy_workqueue' (function is undefined)
Removed calls to 'cdev_del' (function is undefined)
Removed calls to 'platform_device_unregister' (function is undefined)
Removed calls to 'bus_unregister' (function is undefined)
Defining function kobject_uevent_env as symbolic
Defining function __phys_addr as symbolic
Defining function __alloc_workqueue_key as symbolic
Defining function platform_device_register as symbolic
Defining function bus_register as symbolic
Defining function alloc_chrdev_region as symbolic
Defining function cdev_add as symbolic
Removed calls to '__might_fault' (function is undefined)
Defining function remap_pfn_range as symbolic
Defining function _copy_from_user as symbolic
Defining function _copy_to_user as symbolic
Defining function queue_work_on as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'acpi_bus_unregister_driver' (function is undefined)
Removed calls to 'ldv_check_final_state' (function is undefined)
Defining function ldv_probe_6 as symbolic
Defining function acpi_bus_register_driver as symbolic
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  memcmp
  strcmp
  strlen
  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.972466945648
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 475 289 1387 13534
INFO: Starting verification
KLEE: WARNING ONCE: function "visordriver_probe_device" has inline asm
KLEE: WARNING ONCE: function "visordriver_remove_device" has inline asm
KLEE: WARNING ONCE: function "signalremove_inner" has inline asm
KLEE: WARNING ONCE: function "signalinsert_inner" has inline asm
KLEE: WARNING ONCE: function "__unisys_extended_vmcall_gnuc" has inline asm
KLEE: WARNING ONCE: function "cpuid" has inline asm
KLEE: WARNING ONCE: function "spar_check_channel_client" has inline asm
KLEE: WARNING ONCE: function "controlvm_periodic_work" has inline asm
KLEE: WARNING ONCE: function "__unisys_vmcall_gnuc" has inline asm
KLEE: WARNING: undefined reference to function: delayed_work_timer_fn
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_3fdaea0d-a0ea-4bcb-8fc9-2486d6b9eb40/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-rclfMz/linux-4.2-rc1.tar.xz-43_2a-drivers--staging--unisys--visorbus--visorbus.ko-entry_point_true-unreach-call.cil.out.c:6266: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-rclfMz/linux-4.2-rc1.tar.xz-43_2a-drivers--staging--unisys--visorbus--visorbus.ko-entry_point_true-unreach-call.cil.out.c:6273: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 31184 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 34591 states (over memory cap)
KLEE: WARNING: killing 31437 states (over memory cap)
KLEE: WARNING: killing 30881 states (over memory cap)
KLEE: WARNING: killing 30463 states (over memory cap)
KLEE: WARNING: killing 30321 states (over memory cap)
KLEE: WARNING: killing 28182 states (over memory cap)
KLEE: WARNING: killing 31061 states (over memory cap)
KLEE: WARNING: killing 31796 states (over memory cap)
KLEE: WARNING: killing 30933 states (over memory cap)
KLEE: WARNING: killing 35557 states (over memory cap)
KLEE: WARNING: killing 36038 states (over memory cap)
KLEE: WARNING: killing 36467 states (over memory cap)
KLEE: WARNING: killing 36169 states (over memory cap)
KLEE: WARNING: killing 35136 states (over memory cap)
KLEE: WARNING: killing 34964 states (over memory cap)
KLEE: WARNING: killing 34255 states (over memory cap)
KLEE: WARNING: killing 33619 states (over memory cap)
KLEE: WARNING: killing 33381 states (over memory cap)
KLEE: WARNING: killing 32410 states (over memory cap)
KLEE: WARNING: killing 33412 states (over memory cap)
KLEE: WARNING: killing 32786 states (over memory cap)
KLEE: WARNING: killing 31878 states (over memory cap)
KLEE: WARNING: killing 31847 states (over memory cap)
KLEE: WARNING: killing 34163 states (over memory cap)
KLEE: WARNING: killing 33981 states (over memory cap)
KLEE: WARNING: killing 35190 states (over memory cap)
KLEE: WARNING: killing 32344 states (over memory cap)
KLEE: WARNING: killing 33415 states (over memory cap)
KLEE: WARNING: killing 35743 states (over memory cap)
KLEE: WARNING: killing 33549 states (over memory cap)
KLEE: WARNING: killing 33912 states (over memory cap)
KLEE: WARNING: killing 31927 states (over memory cap)
KLEE: WARNING: killing 32983 states (over memory cap)
KLEE: WARNING: killing 33915 states (over memory cap)
KLEE: WARNING: killing 33690 states (over memory cap)
KLEE: WARNING: killing 34041 states (over memory cap)
KLEE: WARNING: killing 31990 states (over memory cap)
KLEE: WARNING: killing 33760 states (over memory cap)
KLEE: WARNING: killing 33336 states (over memory cap)
KLEE: WARNING: killing 32707 states (over memory cap)
KLEE: WARNING: killing 34166 states (over memory cap)
KLEE: WARNING: killing 33155 states (over memory cap)
KLEE: WARNING: killing 32746 states (over memory cap)
KLEE: WARNING: killing 33293 states (over memory cap)
KLEE: WARNING: killing 34600 states (over memory cap)
KLEE: WARNING: killing 35204 states (over memory cap)
KLEE: WARNING: killing 33817 states (over memory cap)
KLEE: WARNING: killing 33730 states (over memory cap)
KLEE: WARNING: killing 34137 states (over memory cap)
KLEE: WARNING: killing 32564 states (over memory cap)
KLEE: WARNING: killing 32453 states (over memory cap)
KLEE: WARNING: killing 33828 states (over memory cap)
KLEE: WARNING: killing 32630 states (over memory cap)
KLEE: WARNING: killing 35136 states (over memory cap)
KLEE: WARNING: killing 32755 states (over memory cap)
KLEE: WARNING: killing 33094 states (over memory cap)
KLEE: WARNING: killing 33126 states (over memory cap)
KLEE: WARNING: killing 33014 states (over memory cap)
KLEE: WARNING: killing 32344 states (over memory cap)
KLEE: WARNING: killing 33250 states (over memory cap)
KLEE: WARNING: killing 33847 states (over memory cap)
KLEE: WARNING: killing 33062 states (over memory cap)
KLEE: WARNING: killing 35178 states (over memory cap)
KLEE: WARNING: killing 32184 states (over memory cap)
KLEE: WARNING: killing 34278 states (over memory cap)
KLEE: WARNING: killing 33239 states (over memory cap)
KLEE: WARNING: killing 33521 states (over memory cap)
KLEE: WARNING: killing 33353 states (over memory cap)
KLEE: WARNING: killing 32692 states (over memory cap)
KLEE: WARNING: killing 34285 states (over memory cap)
KLEE: WARNING: killing 34938 states (over memory cap)
KLEE: WARNING: killing 32477 states (over memory cap)
KLEE: WARNING: killing 35070 states (over memory cap)
KLEE: WARNING: killing 31977 states (over memory cap)
KLEE: WARNING: killing 32433 states (over memory cap)
KLEE: WARNING: killing 33777 states (over memory cap)
KLEE: WARNING: killing 33185 states (over memory cap)
KLEE: WARNING: killing 34011 states (over memory cap)
KLEE: WARNING: killing 32001 states (over memory cap)
KLEE: WARNING: killing 33450 states (over memory cap)
KLEE: WARNING: killing 33289 states (over memory cap)
KLEE: WARNING: killing 34068 states (over memory cap)
KLEE: WARNING: killing 35586 states (over memory cap)
KLEE: WARNING: killing 32950 states (over memory cap)
KLEE: WARNING: killing 32973 states (over memory cap)
KLEE: WARNING: killing 32946 states (over memory cap)
KLEE: WARNING: killing 33287 states (over memory cap)
KLEE: WARNING: killing 33438 states (over memory cap)
KLEE: WARNING: killing 35873 states (over memory cap)
KLEE: WARNING: killing 34608 states (over memory cap)
KLEE: WARNING: killing 35138 states (over memory cap)
KLEE: WARNING: killing 32229 states (over memory cap)
KLEE: WARNING: killing 33118 states (over memory cap)
KLEE: WARNING: killing 32658 states (over memory cap)
KLEE: WARNING: killing 31845 states (over memory cap)
KLEE: WARNING: killing 33691 states (over memory cap)
KLEE: WARNING: killing 33606 states (over memory cap)
KLEE: WARNING: killing 33281 states (over memory cap)
KLEE: WARNING: killing 32387 states (over memory cap)
KLEE: WARNING: killing 33323 states (over memory cap)
KLEE: WARNING: killing 33611 states (over memory cap)
KLEE: WARNING: killing 33890 states (over memory cap)
KLEE: WARNING: killing 34578 states (over memory cap)
KLEE: WARNING: killing 32865 states (over memory cap)
KLEE: WARNING: killing 32717 states (over memory cap)
KLEE: WARNING: killing 35772 states (over memory cap)
KLEE: WARNING: killing 32110 states (over memory cap)
