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--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 320 2490 15402
Removed infinite loop in __cpuid
Removed infinite loop in __cpuid___0
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 0.621170043945
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 '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.758933782578
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 471 276 1353 13393
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_08284cba-cd80-4c3a-8b67-cfd4f06d8233/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-J9zk05/linux-4.2-rc1.tar.xz-08_1a-drivers--staging--unisys--visorbus--visorbus.ko-entry_point_true-unreach-call.cil.out.c:10654: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-J9zk05/linux-4.2-rc1.tar.xz-08_1a-drivers--staging--unisys--visorbus--visorbus.ko-entry_point_true-unreach-call.cil.out.c:10661: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 31165 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 32416 states (over memory cap)
KLEE: WARNING: killing 30131 states (over memory cap)
KLEE: WARNING: killing 30113 states (over memory cap)
KLEE: WARNING: killing 29211 states (over memory cap)
KLEE: WARNING: killing 31113 states (over memory cap)
KLEE: WARNING: killing 30168 states (over memory cap)
KLEE: WARNING: killing 29630 states (over memory cap)
KLEE: WARNING: killing 31660 states (over memory cap)
KLEE: WARNING: killing 33023 states (over memory cap)
KLEE: WARNING: killing 33906 states (over memory cap)
KLEE: WARNING: killing 35819 states (over memory cap)
KLEE: WARNING: killing 35715 states (over memory cap)
KLEE: WARNING: killing 36265 states (over memory cap)
KLEE: WARNING: killing 36225 states (over memory cap)
KLEE: WARNING: killing 35785 states (over memory cap)
KLEE: WARNING: killing 32067 states (over memory cap)
KLEE: WARNING: killing 31413 states (over memory cap)
KLEE: WARNING: killing 34516 states (over memory cap)
KLEE: WARNING: killing 32591 states (over memory cap)
KLEE: WARNING: killing 32351 states (over memory cap)
KLEE: WARNING: killing 34317 states (over memory cap)
KLEE: WARNING: killing 33327 states (over memory cap)
KLEE: WARNING: killing 33352 states (over memory cap)
KLEE: WARNING: killing 34455 states (over memory cap)
KLEE: WARNING: killing 34611 states (over memory cap)
KLEE: WARNING: killing 33516 states (over memory cap)
KLEE: WARNING: killing 32754 states (over memory cap)
KLEE: WARNING: killing 33574 states (over memory cap)
KLEE: WARNING: killing 31494 states (over memory cap)
KLEE: WARNING: killing 35473 states (over memory cap)
KLEE: WARNING: killing 33650 states (over memory cap)
KLEE: WARNING: killing 33152 states (over memory cap)
KLEE: WARNING: killing 34034 states (over memory cap)
KLEE: WARNING: killing 32226 states (over memory cap)
KLEE: WARNING: killing 33627 states (over memory cap)
KLEE: WARNING: killing 32740 states (over memory cap)
KLEE: WARNING: killing 33701 states (over memory cap)
KLEE: WARNING: killing 33073 states (over memory cap)
KLEE: WARNING: killing 34541 states (over memory cap)
KLEE: WARNING: killing 30972 states (over memory cap)
KLEE: WARNING: killing 34138 states (over memory cap)
KLEE: WARNING: killing 32200 states (over memory cap)
KLEE: WARNING: killing 32887 states (over memory cap)
KLEE: WARNING: killing 33493 states (over memory cap)
KLEE: WARNING: killing 34903 states (over memory cap)
KLEE: WARNING: killing 33624 states (over memory cap)
KLEE: WARNING: killing 31768 states (over memory cap)
KLEE: WARNING: killing 34527 states (over memory cap)
KLEE: WARNING: killing 33768 states (over memory cap)
KLEE: WARNING: killing 33093 states (over memory cap)
KLEE: WARNING: killing 33128 states (over memory cap)
KLEE: WARNING: killing 32303 states (over memory cap)
KLEE: WARNING: killing 32848 states (over memory cap)
KLEE: WARNING: killing 34485 states (over memory cap)
KLEE: WARNING: killing 33416 states (over memory cap)
KLEE: WARNING: killing 34278 states (over memory cap)
KLEE: WARNING: killing 32762 states (over memory cap)
KLEE: WARNING: killing 32983 states (over memory cap)
KLEE: WARNING: killing 34303 states (over memory cap)
KLEE: WARNING: killing 33937 states (over memory cap)
KLEE: WARNING: killing 31533 states (over memory cap)
KLEE: WARNING: killing 31626 states (over memory cap)
KLEE: WARNING: killing 33438 states (over memory cap)
KLEE: WARNING: killing 34228 states (over memory cap)
KLEE: WARNING: killing 33622 states (over memory cap)
KLEE: WARNING: killing 33400 states (over memory cap)
KLEE: WARNING: killing 34887 states (over memory cap)
KLEE: WARNING: killing 33139 states (over memory cap)
KLEE: WARNING: killing 32964 states (over memory cap)
KLEE: WARNING: killing 32307 states (over memory cap)
KLEE: WARNING: killing 33033 states (over memory cap)
KLEE: WARNING: killing 33438 states (over memory cap)
KLEE: WARNING: killing 33408 states (over memory cap)
KLEE: WARNING: killing 34761 states (over memory cap)
KLEE: WARNING: killing 32778 states (over memory cap)
KLEE: WARNING: killing 31920 states (over memory cap)
KLEE: WARNING: killing 33722 states (over memory cap)
KLEE: WARNING: killing 34053 states (over memory cap)
KLEE: WARNING: killing 34018 states (over memory cap)
KLEE: WARNING: killing 33183 states (over memory cap)
KLEE: WARNING: killing 33396 states (over memory cap)
KLEE: WARNING: killing 32916 states (over memory cap)
KLEE: WARNING: killing 33461 states (over memory cap)
KLEE: WARNING: killing 34608 states (over memory cap)
KLEE: WARNING: killing 32765 states (over memory cap)
KLEE: WARNING: killing 34788 states (over memory cap)
KLEE: WARNING: killing 33021 states (over memory cap)
KLEE: WARNING: killing 34357 states (over memory cap)
KLEE: WARNING: killing 31343 states (over memory cap)
KLEE: WARNING: killing 34169 states (over memory cap)
KLEE: WARNING: killing 34764 states (over memory cap)
KLEE: WARNING: killing 33128 states (over memory cap)
KLEE: WARNING: killing 33027 states (over memory cap)
KLEE: WARNING: killing 33183 states (over memory cap)
KLEE: WARNING: killing 31661 states (over memory cap)
KLEE: WARNING: killing 35026 states (over memory cap)
KLEE: WARNING: killing 33335 states (over memory cap)
KLEE: WARNING: killing 33682 states (over memory cap)
KLEE: WARNING: killing 32727 states (over memory cap)
KLEE: WARNING: killing 34183 states (over memory cap)
KLEE: WARNING: killing 34892 states (over memory cap)
KLEE: WARNING: killing 34362 states (over memory cap)
KLEE: WARNING: killing 34465 states (over memory cap)
KLEE: WARNING: killing 33998 states (over memory cap)
KLEE: WARNING: killing 32183 states (over memory cap)
KLEE: WARNING: killing 32706 states (over memory cap)
KLEE: WARNING: killing 32734 states (over memory cap)
KLEE: WARNING: killing 33813 states (over memory cap)
KLEE: WARNING: killing 31940 states (over memory cap)
KLEE: WARNING: killing 33629 states (over memory cap)
