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--mtd--mtd.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.: 292 219 2520 16085
Removed infinite loop in add_mtd_device
Removed infinite loop in allocate_partition
Removed infinite loop in __put_mtd_device
Removed infinite loop in concat_erase
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 0.699695110321
Defining function idr_get_next as symbolic
Defining function kmemdup as symbolic
Defining function register_reboot_notifier as symbolic
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'idr_remove' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to 'device_unregister' (function is undefined)
Defining function printk as symbolic
Defining function debug_lockdep_rcu_enabled as symbolic
Defining function idr_find_slowpath as symbolic
Defining function sysfs_create_files as symbolic
Defining function kstrdup as symbolic
Defining function idr_alloc as symbolic
Defining function dev_set_name as symbolic
Defining function device_register as symbolic
Defining function device_create as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function __request_module as symbolic
Defining function unregister_reboot_notifier as symbolic
Removed calls to 'list_del' (function is undefined)
Removed calls to 'bdput' (function is undefined)
Removed calls to 'deactivate_locked_super' (function is undefined)
Removed calls to 'lockref_get' (function is undefined)
Defining function lookup_bdev as symbolic
Defining function sget as symbolic
Removed calls to 'generic_shutdown_super' (function is undefined)
Removed calls to 'add_wait_queue' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'remove_wait_queue' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Defining function default_wake_function as symbolic
Removed calls to '__wake_up' (function is undefined)
Removed calls to 'sysfs_remove_files' (function is undefined)
Removed calls to 'device_destroy' (function is undefined)
Defining function snprintf as symbolic
Defining function kstrtouint as symbolic
Defining function seq_lseek as symbolic
Defining function seq_read as symbolic
Defining function single_release as symbolic
Defining function single_open as symbolic
Defining function seq_puts as symbolic
Defining function seq_printf as symbolic
Removed calls to '__might_fault' (function is undefined)
Removed calls to '__copy_from_user_overflow' (function is undefined)
Removed calls to '__copy_to_user_overflow' (function is undefined)
Defining function capable as symbolic
Defining function memdup_user as symbolic
Defining function _copy_to_user as symbolic
Defining function _copy_from_user as symbolic
Defining function fixed_size_llseek as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to '__unregister_chrdev' (function is undefined)
Removed calls to 'remove_proc_entry' (function is undefined)
Removed calls to 'class_unregister' (function is undefined)
Removed calls to 'bdi_destroy' (function is undefined)
Defining function ldv_suspend_late_21 as symbolic
Defining function ldv_restore_early_21 as symbolic
Defining function ldv_resume_early_21 as symbolic
Defining function ldv_thaw_early_21 as symbolic
Defining function ldv_resume_noirq_21 as symbolic
Defining function ldv_freeze_noirq_21 as symbolic
Defining function ldv_prepare_21 as symbolic
Defining function ldv_freeze_late_21 as symbolic
Defining function ldv_thaw_noirq_21 as symbolic
Defining function ldv_poweroff_noirq_21 as symbolic
Defining function ldv_poweroff_late_21 as symbolic
Defining function ldv_restore_noirq_21 as symbolic
Defining function ldv_suspend_noirq_21 as symbolic
Defining function ldv_complete_21 as symbolic
Defining function ldv_probe_4 as symbolic
Defining function __class_register as symbolic
Defining function __register_chrdev as symbolic
Defining function proc_create_data as symbolic
Defining function bdi_init as symbolic
Defining function bdi_register as symbolic
Linked our definitions to these undefined functions:
  strcmp
  __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.740373849869
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 432 231 1420 10199
INFO: Starting verification
KLEE: WARNING ONCE: function "add_mtd_device" has inline asm
KLEE: WARNING ONCE: function "allocate_partition" has inline asm
KLEE: WARNING ONCE: function "__put_mtd_device" has inline asm
KLEE: WARNING ONCE: function "concat_erase" has inline asm
KLEE: WARNING ONCE: function "mtdchar_writeoob" has inline asm
KLEE: WARNING ONCE: function "mtdchar_readoob" has inline asm
KLEE: WARNING ONCE: function "mtdchar_ioctl" 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_c8907a95-b356-4a83-994d-5d7dfc2dc67f/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 10915 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 26133 states (over memory cap)
KLEE: WARNING: killing 24951 states (over memory cap)
KLEE: WARNING: killing 24688 states (over memory cap)
KLEE: WARNING: killing 24079 states (over memory cap)
KLEE: WARNING: killing 23130 states (over memory cap)
KLEE: WARNING: killing 23782 states (over memory cap)
KLEE: WARNING: killing 23083 states (over memory cap)
KLEE: WARNING: killing 26025 states (over memory cap)
KLEE: WARNING: killing 27034 states (over memory cap)
KLEE: WARNING: killing 27947 states (over memory cap)
KLEE: WARNING: killing 27170 states (over memory cap)
KLEE: WARNING: killing 28045 states (over memory cap)
KLEE: WARNING: killing 26528 states (over memory cap)
KLEE: WARNING: killing 24911 states (over memory cap)
KLEE: WARNING: killing 26025 states (over memory cap)
KLEE: WARNING: killing 25054 states (over memory cap)
KLEE: WARNING: killing 25317 states (over memory cap)
KLEE: WARNING: killing 25430 states (over memory cap)
KLEE: WARNING: killing 25648 states (over memory cap)
KLEE: WARNING: killing 26115 states (over memory cap)
KLEE: WARNING: killing 26227 states (over memory cap)
KLEE: WARNING: killing 26834 states (over memory cap)
KLEE: WARNING: killing 26129 states (over memory cap)
KLEE: WARNING: killing 25558 states (over memory cap)
KLEE: WARNING: killing 27941 states (over memory cap)
KLEE: WARNING: killing 24929 states (over memory cap)
KLEE: WARNING: killing 25683 states (over memory cap)
KLEE: WARNING: killing 26381 states (over memory cap)
KLEE: WARNING: killing 26698 states (over memory cap)
KLEE: WARNING: killing 25788 states (over memory cap)
KLEE: WARNING: killing 26111 states (over memory cap)
KLEE: WARNING: killing 25737 states (over memory cap)
KLEE: WARNING: killing 25668 states (over memory cap)
KLEE: WARNING: killing 25302 states (over memory cap)
KLEE: WARNING: killing 26051 states (over memory cap)
KLEE: WARNING: killing 25635 states (over memory cap)
KLEE: WARNING: killing 26909 states (over memory cap)
KLEE: WARNING: killing 26412 states (over memory cap)
KLEE: WARNING: killing 26336 states (over memory cap)
KLEE: WARNING: killing 26021 states (over memory cap)
KLEE: WARNING: killing 26474 states (over memory cap)
KLEE: WARNING: killing 25005 states (over memory cap)
KLEE: WARNING: killing 26183 states (over memory cap)
KLEE: WARNING: killing 26007 states (over memory cap)
KLEE: WARNING: killing 27079 states (over memory cap)
KLEE: WARNING: killing 26091 states (over memory cap)
KLEE: WARNING: killing 25202 states (over memory cap)
KLEE: WARNING: killing 25844 states (over memory cap)
KLEE: WARNING: killing 26106 states (over memory cap)
KLEE: WARNING: killing 27369 states (over memory cap)
KLEE: WARNING: killing 24722 states (over memory cap)
KLEE: WARNING: killing 26118 states (over memory cap)
KLEE: WARNING: killing 26579 states (over memory cap)
KLEE: WARNING: killing 25977 states (over memory cap)
KLEE: WARNING: killing 25287 states (over memory cap)
KLEE: WARNING: killing 26261 states (over memory cap)
KLEE: WARNING: killing 26713 states (over memory cap)
KLEE: WARNING: killing 27544 states (over memory cap)
KLEE: WARNING: killing 24762 states (over memory cap)
KLEE: WARNING: killing 26207 states (over memory cap)
KLEE: WARNING: killing 26334 states (over memory cap)
KLEE: WARNING: killing 25221 states (over memory cap)
KLEE: WARNING: killing 26322 states (over memory cap)
KLEE: WARNING: killing 24087 states (over memory cap)
KLEE: WARNING: killing 25332 states (over memory cap)
KLEE: WARNING: killing 26387 states (over memory cap)
KLEE: WARNING: killing 25566 states (over memory cap)
KLEE: WARNING: killing 26586 states (over memory cap)
KLEE: WARNING: killing 25949 states (over memory cap)
KLEE: WARNING: killing 26769 states (over memory cap)
KLEE: WARNING: killing 26286 states (over memory cap)
KLEE: WARNING: killing 26350 states (over memory cap)
KLEE: WARNING: killing 26133 states (over memory cap)
KLEE: WARNING: killing 25932 states (over memory cap)
KLEE: WARNING: killing 26051 states (over memory cap)
KLEE: WARNING: killing 25602 states (over memory cap)
KLEE: WARNING: killing 25675 states (over memory cap)
KLEE: WARNING: killing 26263 states (over memory cap)
KLEE: WARNING: killing 26237 states (over memory cap)
KLEE: WARNING: killing 26265 states (over memory cap)
KLEE: WARNING: killing 26383 states (over memory cap)
KLEE: WARNING: killing 26315 states (over memory cap)
KLEE: WARNING: killing 26984 states (over memory cap)
KLEE: WARNING: killing 25533 states (over memory cap)
KLEE: WARNING: killing 25220 states (over memory cap)
KLEE: WARNING: killing 27255 states (over memory cap)
KLEE: WARNING: killing 25604 states (over memory cap)
KLEE: WARNING: killing 26562 states (over memory cap)
KLEE: WARNING: killing 25295 states (over memory cap)
KLEE: WARNING: killing 25920 states (over memory cap)
KLEE: WARNING: killing 27423 states (over memory cap)
KLEE: WARNING: killing 25645 states (over memory cap)
KLEE: WARNING: killing 24337 states (over memory cap)
KLEE: WARNING: killing 25742 states (over memory cap)
KLEE: WARNING: killing 25620 states (over memory cap)
KLEE: WARNING: killing 25325 states (over memory cap)
KLEE: WARNING: killing 26496 states (over memory cap)
KLEE: WARNING: killing 26111 states (over memory cap)
KLEE: WARNING: killing 26239 states (over memory cap)
KLEE: WARNING: killing 27321 states (over memory cap)
KLEE: WARNING: killing 26210 states (over memory cap)
KLEE: WARNING: killing 26178 states (over memory cap)
KLEE: WARNING: killing 26121 states (over memory cap)
KLEE: WARNING: killing 24860 states (over memory cap)
KLEE: WARNING: killing 26587 states (over memory cap)
KLEE: WARNING: killing 25182 states (over memory cap)
KLEE: WARNING: killing 26169 states (over memory cap)
KLEE: WARNING: killing 25135 states (over memory cap)
KLEE: WARNING: killing 26758 states (over memory cap)
KLEE: WARNING: killing 25785 states (over memory cap)
KLEE: WARNING: killing 26636 states (over memory cap)
KLEE: WARNING: killing 25205 states (over memory cap)
KLEE: WARNING: killing 24816 states (over memory cap)
KLEE: WARNING: killing 27256 states (over memory cap)
KLEE: WARNING: killing 25367 states (over memory cap)
KLEE: WARNING: killing 25889 states (over memory cap)
KLEE: WARNING: killing 26182 states (over memory cap)
KLEE: WARNING: killing 26392 states (over memory cap)
KLEE: WARNING: killing 26100 states (over memory cap)
KLEE: WARNING: killing 26893 states (over memory cap)
KLEE: WARNING: killing 26324 states (over memory cap)
KLEE: WARNING: killing 25988 states (over memory cap)
