bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-challenges/linux-3.14__complex_emg__linux-kernel-locking-spinlock__drivers-net-can-softing-softing_true-unreach-call.cil.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.: 215 355 2316 12521
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.599849939346
Removed calls to '_raw_spin_lock_bh' (function is undefined)
Removed calls to 'iowrite8' (function is undefined)
Removed calls to 'can_bus_off' (function is undefined)
Removed calls to '_raw_spin_unlock_bh' (function is undefined)
Defining function netpoll_trap as symbolic
Defining function ioread8 as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function can_get_echo_skb as symbolic
Defining function printk as symbolic
Defining function ktime_get as symbolic
Defining function ktime_get_real as symbolic
Defining function alloc_can_skb as symbolic
Defining function netif_rx as symbolic
Defining function sprintf as symbolic
Removed calls to 'mutex_unlock' (function is undefined)
Defining function mutex_lock_interruptible_nested as symbolic
Defining function kstrtoull as symbolic
Defining function open_candev as symbolic
Removed calls to 'close_candev' (function is undefined)
Removed calls to 'iowrite16' (function is undefined)
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'ldv_free_irq' (function is undefined)
Defining function dev_alert as symbolic
Defining function dev_close as symbolic
Removed calls to 'usleep_range' (function is undefined)
Defining function ioread16 as symbolic
Defining function request_threaded_irq as symbolic
Removed calls to 'kfree_skb' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to 'can_put_echo_skb' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'platform_driver_unregister' (function is undefined)
Defining function __platform_driver_register as symbolic
Removed calls to 'ldv_check_alloc_flags' (function is undefined)
Removed calls to 'ldv_after_alloc' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'free_candev' (function is undefined)
Removed calls to 'sysfs_remove_group' (function is undefined)
Removed calls to 'iounmap' (function is undefined)
Removed calls to 'unregister_candev' (function is undefined)
Defining function dev_warn as symbolic
Defining function platform_get_resource as symbolic
Defining function ioremap_nocache as symbolic
Defining function sysfs_create_group as symbolic
Defining function _dev_info as symbolic
Defining function register_candev as symbolic
Defining function alloc_candev as symbolic
Removed calls to 'release_firmware' (function is undefined)
Removed calls to 'iowrite32' (function is undefined)
Defining function ioread32 as symbolic
Defining function request_firmware as symbolic
Defining function __dynamic_dev_dbg as symbolic
Defining function krealloc as symbolic
Defining function external_allocated_data as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'ldv_switch_to_interrupt_context' (function is undefined)
Removed calls to 'ldv_switch_to_process_context' (function is undefined)
Removed calls to 'ldv_pre_probe' (function is undefined)
Removed calls to 'ldv_assert' (function is undefined)
Linked our definitions to these undefined functions:
  memcmp
  strncmp
  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.600234031677
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 284 338 1239 7288
INFO: Starting verification
KLEE: WARNING ONCE: function "softing_irq_thread" has inline asm
KLEE: WARNING ONCE: function "netif_stop_queue" has inline asm
KLEE: WARNING ONCE: function "softing_startstop" has inline asm
KLEE: WARNING ONCE: function "softing_reset_chip" has inline asm
KLEE: WARNING ONCE: function "_softing_fct_cmd" has inline asm
KLEE: WARNING ONCE: function "softing_pdev_probe" has inline asm
KLEE: WARNING ONCE: function "softing_load_fw" has inline asm
KLEE: WARNING ONCE: function "softing_bootloader_command" has inline asm
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_e6366b1a-5660-4ee7-8b3d-1f0ae1bde614/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: WARNING ONCE: flushing 10568 bytes on read, may be slow and/or crash: MO171[10568] allocated at global:
KLEE: ERROR: /tmp/symbiotic-e64S8b/linux-3.14__complex_emg__linux-kernel-locking-spinlock__drivers-net-can-softing-softing_true-unreach-call.cil.c:7184: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 26695 states (over memory cap)
KLEE: WARNING: killing 17418 states (over memory cap)
KLEE: WARNING: killing 17218 states (over memory cap)
KLEE: WARNING: killing 18249 states (over memory cap)
KLEE: WARNING: killing 17603 states (over memory cap)
KLEE: WARNING: killing 16954 states (over memory cap)
KLEE: WARNING: killing 16771 states (over memory cap)
KLEE: WARNING: killing 15974 states (over memory cap)
KLEE: WARNING: killing 16391 states (over memory cap)
KLEE: WARNING: killing 16059 states (over memory cap)
KLEE: WARNING: killing 16481 states (over memory cap)
KLEE: WARNING: killing 16444 states (over memory cap)
KLEE: WARNING: killing 16265 states (over memory cap)
KLEE: WARNING: killing 16686 states (over memory cap)
KLEE: WARNING: killing 16505 states (over memory cap)
KLEE: WARNING: killing 16172 states (over memory cap)
KLEE: WARNING: killing 16596 states (over memory cap)
KLEE: WARNING: killing 17457 states (over memory cap)
KLEE: WARNING: killing 16982 states (over memory cap)
KLEE: WARNING: killing 17696 states (over memory cap)
KLEE: WARNING: killing 17513 states (over memory cap)
KLEE: WARNING: killing 18085 states (over memory cap)
KLEE: WARNING: killing 17458 states (over memory cap)
KLEE: WARNING: killing 17138 states (over memory cap)
KLEE: WARNING: killing 17995 states (over memory cap)
KLEE: WARNING: killing 17961 states (over memory cap)
KLEE: WARNING: killing 17498 states (over memory cap)
KLEE: WARNING: killing 18344 states (over memory cap)
KLEE: WARNING: killing 19191 states (over memory cap)
KLEE: WARNING: killing 19756 states (over memory cap)
KLEE: WARNING: killing 18848 states (over memory cap)
KLEE: WARNING: killing 18829 states (over memory cap)
KLEE: WARNING: killing 18655 states (over memory cap)
KLEE: WARNING: killing 19945 states (over memory cap)
KLEE: WARNING: killing 19191 states (over memory cap)
KLEE: WARNING: killing 17859 states (over memory cap)
KLEE: WARNING: killing 18991 states (over memory cap)
KLEE: WARNING: killing 19258 states (over memory cap)
KLEE: WARNING: killing 19084 states (over memory cap)
KLEE: WARNING: killing 18635 states (over memory cap)
KLEE: WARNING: killing 18758 states (over memory cap)
KLEE: WARNING: killing 18592 states (over memory cap)
KLEE: WARNING: killing 18139 states (over memory cap)
KLEE: WARNING: killing 19124 states (over memory cap)
KLEE: WARNING: killing 18386 states (over memory cap)
KLEE: WARNING: killing 18358 states (over memory cap)
KLEE: WARNING: killing 18192 states (over memory cap)
KLEE: WARNING: killing 17886 states (over memory cap)
KLEE: WARNING: killing 18154 states (over memory cap)
KLEE: WARNING: killing 18415 states (over memory cap)
KLEE: WARNING: killing 17397 states (over memory cap)
KLEE: WARNING: killing 19075 states (over memory cap)
KLEE: WARNING: killing 17216 states (over memory cap)
KLEE: WARNING: killing 18469 states (over memory cap)
KLEE: WARNING: killing 18023 states (over memory cap)
KLEE: WARNING: killing 17997 states (over memory cap)
KLEE: WARNING: killing 17983 states (over memory cap)
KLEE: WARNING: killing 17397 states (over memory cap)
KLEE: WARNING: killing 17515 states (over memory cap)
KLEE: WARNING: killing 17493 states (over memory cap)
KLEE: WARNING: killing 18739 states (over memory cap)
KLEE: WARNING: killing 17453 states (over memory cap)
KLEE: WARNING: killing 18282 states (over memory cap)
KLEE: WARNING: killing 17563 states (over memory cap)
KLEE: WARNING: killing 17815 states (over memory cap)
KLEE: WARNING: killing 17231 states (over memory cap)
KLEE: WARNING: killing 18189 states (over memory cap)
KLEE: WARNING: killing 17888 states (over memory cap)
KLEE: WARNING: killing 18146 states (over memory cap)
KLEE: WARNING: killing 18120 states (over memory cap)
KLEE: WARNING: killing 17825 states (over memory cap)
KLEE: WARNING: killing 18511 states (over memory cap)
KLEE: WARNING: killing 18776 states (over memory cap)
KLEE: WARNING: killing 18063 states (over memory cap)
KLEE: WARNING: killing 17478 states (over memory cap)
KLEE: WARNING: killing 17879 states (over memory cap)
KLEE: WARNING: killing 17996 states (over memory cap)
KLEE: WARNING: killing 17420 states (over memory cap)
KLEE: WARNING: killing 17402 states (over memory cap)
KLEE: WARNING: killing 17376 states (over memory cap)
KLEE: WARNING: killing 18469 states (over memory cap)
KLEE: WARNING: killing 18036 states (over memory cap)
KLEE: WARNING: killing 18975 states (over memory cap)
KLEE: WARNING: killing 18679 states (over memory cap)
KLEE: WARNING: killing 17710 states (over memory cap)
KLEE: WARNING: killing 18367 states (over memory cap)
KLEE: WARNING: killing 17529 states (over memory cap)
KLEE: WARNING: killing 19288 states (over memory cap)
KLEE: WARNING: killing 17767 states (over memory cap)
KLEE: WARNING: killing 18433 states (over memory cap)
KLEE: WARNING: killing 17996 states (over memory cap)
KLEE: WARNING: killing 17439 states (over memory cap)
KLEE: WARNING: killing 18369 states (over memory cap)
KLEE: WARNING: killing 16988 states (over memory cap)
KLEE: WARNING: killing 18736 states (over memory cap)
KLEE: WARNING: killing 18045 states (over memory cap)
KLEE: WARNING: killing 18298 states (over memory cap)
KLEE: WARNING: killing 18150 states (over memory cap)
KLEE: WARNING: killing 17857 states (over memory cap)
KLEE: WARNING: killing 18101 states (over memory cap)
KLEE: WARNING: killing 18089 states (over memory cap)
KLEE: WARNING: killing 18203 states (over memory cap)
KLEE: WARNING: killing 18049 states (over memory cap)
KLEE: WARNING: killing 17763 states (over memory cap)
KLEE: WARNING: killing 17747 states (over memory cap)
KLEE: WARNING: killing 18403 states (over memory cap)
KLEE: WARNING: killing 17840 states (over memory cap)
KLEE: WARNING: killing 18620 states (over memory cap)
KLEE: WARNING: killing 18477 states (over memory cap)
KLEE: WARNING: killing 17510 states (over memory cap)
KLEE: WARNING: killing 17364 states (over memory cap)
KLEE: WARNING: killing 18018 states (over memory cap)
KLEE: WARNING: killing 17724 states (over memory cap)
KLEE: WARNING: killing 17714 states (over memory cap)
KLEE: WARNING: killing 19028 states (over memory cap)
KLEE: WARNING: killing 18479 states (over memory cap)
KLEE: WARNING: killing 18460 states (over memory cap)
KLEE: WARNING: killing 18311 states (over memory cap)
KLEE: WARNING: killing 18702 states (over memory cap)
KLEE: WARNING: killing 17620 states (over memory cap)
KLEE: WARNING: killing 17598 states (over memory cap)
KLEE: WARNING: killing 17846 states (over memory cap)
KLEE: WARNING: killing 17955 states (over memory cap)
KLEE: WARNING: killing 17414 states (over memory cap)
KLEE: WARNING: killing 17920 states (over memory cap)
KLEE: WARNING: killing 17639 states (over memory cap)
KLEE: WARNING: killing 18016 states (over memory cap)
KLEE: WARNING: killing 17732 states (over memory cap)
KLEE: WARNING: killing 17975 states (over memory cap)
KLEE: WARNING: killing 17429 states (over memory cap)
KLEE: WARNING: killing 17156 states (over memory cap)
KLEE: WARNING: killing 18318 states (over memory cap)
KLEE: WARNING: killing 18040 states (over memory cap)
KLEE: WARNING: killing 17496 states (over memory cap)
KLEE: WARNING: killing 18140 states (over memory cap)
KLEE: WARNING: killing 17721 states (over memory cap)
KLEE: WARNING: killing 17969 states (over memory cap)
KLEE: WARNING: killing 18345 states (over memory cap)
KLEE: WARNING: killing 18200 states (over memory cap)
KLEE: WARNING: killing 18053 states (over memory cap)
KLEE: WARNING: killing 18291 states (over memory cap)
KLEE: WARNING: killing 18799 states (over memory cap)
KLEE: WARNING: killing 17875 states (over memory cap)
KLEE: WARNING: killing 17856 states (over memory cap)
KLEE: WARNING: killing 18096 states (over memory cap)
KLEE: WARNING: killing 18475 states (over memory cap)
KLEE: WARNING: killing 17934 states (over memory cap)
KLEE: WARNING: killing 19081 states (over memory cap)
KLEE: WARNING: killing 17385 states (over memory cap)
KLEE: WARNING: killing 17626 states (over memory cap)
KLEE: WARNING: killing 17733 states (over memory cap)
KLEE: WARNING: killing 18360 states (over memory cap)
KLEE: WARNING: killing 18085 states (over memory cap)
KLEE: WARNING: killing 17300 states (over memory cap)
KLEE: WARNING: killing 18044 states (over memory cap)
KLEE: WARNING: killing 17127 states (over memory cap)
KLEE: WARNING: killing 18005 states (over memory cap)
KLEE: WARNING: killing 18636 states (over memory cap)
KLEE: WARNING: killing 17591 states (over memory cap)
KLEE: WARNING: killing 17571 states (over memory cap)
KLEE: WARNING: killing 17943 states (over memory cap)
KLEE: WARNING: killing 18435 states (over memory cap)
KLEE: WARNING: killing 17778 states (over memory cap)
