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--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.: 366 370 2649 16087
Removed infinite loop in __cpuid
Removed infinite loop in __cpuid___0
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.643642902374
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 __get_free_pages as symbolic
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 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function mutex_trylock as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'acpi_bus_unregister_driver' (function is undefined)
Defining function ldv_probe_6 as symbolic
Defining function acpi_bus_register_driver as symbolic
Linked our definitions to these undefined functions:
  memcmp
  strcmp
  strlen
  __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.780225992203
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 473 327 1528 13880
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 "spar_check_channel_client" has inline asm
KLEE: WARNING ONCE: function "__unisys_extended_vmcall_gnuc___0" has inline asm
KLEE: WARNING ONCE: function "controlvm_periodic_work" has inline asm
KLEE: WARNING ONCE: function "cpuid___0" 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_5c7a7f49-3668-4498-8d6f-31f1b41078fc/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-TXIbFw/linux-4.2-rc1.tar.xz-32_7a-drivers--staging--unisys--visorbus--visorbus.ko-entry_point_true-unreach-call.cil.out.c:10821: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-TXIbFw/linux-4.2-rc1.tar.xz-32_7a-drivers--staging--unisys--visorbus--visorbus.ko-entry_point_true-unreach-call.cil.out.c:10828: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 29154 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 31932 states (over memory cap)
KLEE: WARNING: killing 31982 states (over memory cap)
KLEE: WARNING: killing 29215 states (over memory cap)
KLEE: WARNING: killing 32217 states (over memory cap)
KLEE: WARNING: killing 31255 states (over memory cap)
KLEE: WARNING: killing 29901 states (over memory cap)
KLEE: WARNING: killing 29291 states (over memory cap)
KLEE: WARNING: killing 31258 states (over memory cap)
KLEE: WARNING: killing 32213 states (over memory cap)
KLEE: WARNING: killing 34258 states (over memory cap)
KLEE: WARNING: killing 35688 states (over memory cap)
KLEE: WARNING: killing 34967 states (over memory cap)
KLEE: WARNING: killing 36134 states (over memory cap)
KLEE: WARNING: killing 34213 states (over memory cap)
KLEE: WARNING: killing 34631 states (over memory cap)
KLEE: WARNING: killing 36076 states (over memory cap)
KLEE: WARNING: killing 33957 states (over memory cap)
KLEE: WARNING: killing 34454 states (over memory cap)
KLEE: WARNING: killing 34551 states (over memory cap)
KLEE: WARNING: killing 31230 states (over memory cap)
KLEE: WARNING: killing 30855 states (over memory cap)
KLEE: WARNING: killing 32132 states (over memory cap)
KLEE: WARNING: killing 33698 states (over memory cap)
KLEE: WARNING: killing 31062 states (over memory cap)
KLEE: WARNING: killing 34280 states (over memory cap)
KLEE: WARNING: killing 34164 states (over memory cap)
KLEE: WARNING: killing 33992 states (over memory cap)
KLEE: WARNING: killing 34086 states (over memory cap)
KLEE: WARNING: killing 34193 states (over memory cap)
KLEE: WARNING: killing 33166 states (over memory cap)
KLEE: WARNING: killing 33721 states (over memory cap)
KLEE: WARNING: killing 33289 states (over memory cap)
KLEE: WARNING: killing 31805 states (over memory cap)
KLEE: WARNING: killing 33465 states (over memory cap)
KLEE: WARNING: killing 31796 states (over memory cap)
KLEE: WARNING: killing 34649 states (over memory cap)
KLEE: WARNING: killing 34416 states (over memory cap)
KLEE: WARNING: killing 33789 states (over memory cap)
KLEE: WARNING: killing 32250 states (over memory cap)
KLEE: WARNING: killing 33261 states (over memory cap)
KLEE: WARNING: killing 32044 states (over memory cap)
KLEE: WARNING: killing 35272 states (over memory cap)
KLEE: WARNING: killing 34777 states (over memory cap)
KLEE: WARNING: killing 32078 states (over memory cap)
KLEE: WARNING: killing 32359 states (over memory cap)
KLEE: WARNING: killing 34733 states (over memory cap)
KLEE: WARNING: killing 33591 states (over memory cap)
KLEE: WARNING: killing 33302 states (over memory cap)
KLEE: WARNING: killing 31381 states (over memory cap)
KLEE: WARNING: killing 33795 states (over memory cap)
KLEE: WARNING: killing 33686 states (over memory cap)
KLEE: WARNING: killing 34815 states (over memory cap)
KLEE: WARNING: killing 32516 states (over memory cap)
KLEE: WARNING: killing 33643 states (over memory cap)
KLEE: WARNING: killing 34182 states (over memory cap)
KLEE: WARNING: killing 32676 states (over memory cap)
KLEE: WARNING: killing 34564 states (over memory cap)
KLEE: WARNING: killing 34595 states (over memory cap)
KLEE: WARNING: killing 32942 states (over memory cap)
KLEE: WARNING: killing 32843 states (over memory cap)
KLEE: WARNING: killing 33187 states (over memory cap)
KLEE: WARNING: killing 33343 states (over memory cap)
KLEE: WARNING: killing 32986 states (over memory cap)
KLEE: WARNING: killing 33918 states (over memory cap)
KLEE: WARNING: killing 32973 states (over memory cap)
KLEE: WARNING: killing 33380 states (over memory cap)
KLEE: WARNING: killing 32595 states (over memory cap)
KLEE: WARNING: killing 33314 states (over memory cap)
KLEE: WARNING: killing 32271 states (over memory cap)
KLEE: WARNING: killing 33565 states (over memory cap)
KLEE: WARNING: killing 34162 states (over memory cap)
KLEE: WARNING: killing 34131 states (over memory cap)
KLEE: WARNING: killing 32269 states (over memory cap)
KLEE: WARNING: killing 32859 states (over memory cap)
KLEE: WARNING: killing 34592 states (over memory cap)
KLEE: WARNING: killing 34371 states (over memory cap)
KLEE: WARNING: killing 35406 states (over memory cap)
KLEE: WARNING: killing 32667 states (over memory cap)
KLEE: WARNING: killing 33443 states (over memory cap)
KLEE: WARNING: killing 33546 states (over memory cap)
KLEE: WARNING: killing 32251 states (over memory cap)
KLEE: WARNING: killing 32473 states (over memory cap)
KLEE: WARNING: killing 32953 states (over memory cap)
KLEE: WARNING: killing 33482 states (over memory cap)
KLEE: WARNING: killing 32948 states (over memory cap)
KLEE: WARNING: killing 32799 states (over memory cap)
KLEE: WARNING: killing 33645 states (over memory cap)
KLEE: WARNING: killing 33237 states (over memory cap)
KLEE: WARNING: killing 33136 states (over memory cap)
KLEE: WARNING: killing 35172 states (over memory cap)
KLEE: WARNING: killing 32461 states (over memory cap)
KLEE: WARNING: killing 32740 states (over memory cap)
KLEE: WARNING: killing 32824 states (over memory cap)
KLEE: WARNING: killing 34534 states (over memory cap)
KLEE: WARNING: killing 32956 states (over memory cap)
KLEE: WARNING: killing 33104 states (over memory cap)
KLEE: WARNING: killing 33090 states (over memory cap)
KLEE: WARNING: killing 32818 states (over memory cap)
KLEE: WARNING: killing 34527 states (over memory cap)
KLEE: WARNING: killing 33875 states (over memory cap)
KLEE: WARNING: killing 31378 states (over memory cap)
KLEE: WARNING: killing 33612 states (over memory cap)
KLEE: WARNING: killing 33287 states (over memory cap)
KLEE: WARNING: killing 33204 states (over memory cap)
KLEE: WARNING: killing 33279 states (over memory cap)
KLEE: WARNING: killing 32818 states (over memory cap)
KLEE: WARNING: killing 33768 states (over memory cap)
KLEE: WARNING: killing 34433 states (over memory cap)
KLEE: WARNING: killing 33979 states (over memory cap)
KLEE: WARNING: killing 32712 states (over memory cap)
KLEE: WARNING: killing 32637 states (over memory cap)
KLEE: WARNING: killing 34445 states (over memory cap)
KLEE: WARNING: killing 32825 states (over memory cap)
KLEE: WARNING: killing 32898 states (over memory cap)
KLEE: WARNING: killing 33312 states (over memory cap)
KLEE: WARNING: killing 34817 states (over memory cap)
KLEE: WARNING: killing 33991 states (over memory cap)
KLEE: WARNING: killing 33308 states (over memory cap)
KLEE: WARNING: killing 32654 states (over memory cap)
KLEE: WARNING: killing 34329 states (over memory cap)
KLEE: WARNING: killing 32544 states (over memory cap)
KLEE: WARNING: killing 32198 states (over memory cap)
KLEE: WARNING: killing 35138 states (over memory cap)
KLEE: WARNING: killing 35665 states (over memory cap)
KLEE: WARNING: killing 31999 states (over memory cap)
KLEE: WARNING: killing 34404 states (over memory cap)
