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--crypto--qat--qat_common--intel_qat.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.: 319 436 3358 26191
Removed infinite loop in dma_unmap_single_attrs
Removed infinite loop in dma_map_single_attrs
Removed infinite loop in sg_page
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 0.85933303833
Removed calls to '__init_rwsem' (function is undefined)
Removed calls to 'dev_err' (function is undefined)
Defining function debugfs_create_file as symbolic
Removed calls to 'down_write' (function is undefined)
Removed calls to 'up_write' (function is undefined)
Removed calls to 'debugfs_remove' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Defining function strlcpy as symbolic
Defining function snprintf as symbolic
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function printk as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Defining function request_firmware as symbolic
Removed calls to 'release_firmware' (function is undefined)
Defining function kstrtoull as symbolic
Defining function kmemdup as symbolic
Defining function __memmove as symbolic
Defining function debugfs_create_dir as symbolic
Removed calls to 'down_read' (function is undefined)
Removed calls to 'up_read' (function is undefined)
Defining function kstrtouint as symbolic
Defining function __kmalloc_node as symbolic
Removed calls to '_dev_info' (function is undefined)
Defining function crypto_register_algs as symbolic
Removed calls to 'msleep' (function is undefined)
Defining function crypto_unregister_algs as symbolic
Removed calls to 'dma_free_attrs' (function is undefined)
Defining function pci_enable_pcie_error_reporting as symbolic
Defining function pci_disable_pcie_error_reporting as symbolic
Defining function seq_lseek as symbolic
Defining function seq_read as symbolic
Defining function seq_release as symbolic
Defining function seq_open as symbolic
Defining function seq_printf as symbolic
Defining function seq_list_next as symbolic
Defining function seq_list_start as symbolic
Defining function mutex_lock_interruptible_nested 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 _copy_to_user as symbolic
Defining function _copy_from_user as symbolic
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Defining function pci_cleanup_aer_uncorrect_error_status as symbolic
Removed calls to 'pci_restore_state' (function is undefined)
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Removed calls to 'complete' (function is undefined)
Defining function wait_for_completion_timeout as symbolic
Defining function __msecs_to_jiffies as symbolic
Defining function queue_work_on as symbolic
Defining function pci_wait_for_pending_transaction as symbolic
Defining function pci_save_state as symbolic
Defining function pci_bus_write_config_word as symbolic
Defining function pci_bus_read_config_word as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'crypto_destroy_tfm' (function is undefined)
Removed calls to '_raw_spin_lock_bh' (function is undefined)
Removed calls to '_raw_spin_unlock_bh' (function is undefined)
Removed calls to 'debug_dma_unmap_page' (function is undefined)
Defining function sg_nents as symbolic
Removed calls to 'debug_dma_map_page' (function is undefined)
Removed calls to 'debug_dma_mapping_error' (function is undefined)
Defining function sg_next as symbolic
Defining function __phys_addr as symbolic
Defining function dma_alloc_attrs as symbolic
Defining function crypto_alloc_shash as symbolic
Defining function crypto_authenc_extractkeys as symbolic
Removed calls to 'memzero_explicit' (function is undefined)
Defining function crypto_shash_digest as symbolic
Defining function crypto_shash_update as symbolic
Defining function seq_puts as symbolic
Defining function queue_delayed_work_on as symbolic
Removed calls to 'flush_workqueue' (function is undefined)
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'crypto_put_default_rng' (function is undefined)
Removed calls to 'mutex_destroy' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'cdev_init' (function is undefined)
Removed calls to 'cdev_del' (function is undefined)
Removed calls to 'class_destroy' (function is undefined)
Removed calls to 'unregister_chrdev_region' (function is undefined)
Defining function ldv_open_7 as symbolic
Defining function ldv_release_7 as symbolic
Removed calls to 'destroy_workqueue' (function is undefined)
Removed calls to 'device_destroy' (function is undefined)
Defining function __alloc_workqueue_key as symbolic
Defining function alloc_chrdev_region as symbolic
Defining function __class_create as symbolic
Defining function cdev_add as symbolic
Defining function device_create as symbolic
Defining function crypto_get_default_rng as symbolic
Defining function ldv_suspend_6 as symbolic
Defining function ldv_release_6 as symbolic
Defining function ldv_probe_6 as symbolic
Linked our definitions to these undefined functions:
  strcmp
  strncmp
  strncpy
  __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.998731136322
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 411 332 1933 15945
INFO: Starting verification
KLEE: WARNING ONCE: function "adf_dev_init" has inline asm
KLEE: WARNING ONCE: function "adf_init_etr_data" has inline asm
KLEE: WARNING ONCE: function "adf_ae_init" has inline asm
KLEE: WARNING ONCE: function "qat_uclo_map_uof_obj" has inline asm
KLEE: WARNING ONCE: function "qat_uclo_wr_all_uimage" has inline asm
KLEE: WARNING ONCE: function "qat_hal_wr_umem" has inline asm
KLEE: WARNING ONCE: function "qat_hal_rd_ae_csr" has inline asm
KLEE: WARNING ONCE: function "qat_hal_wr_ae_csr" has inline asm
KLEE: WARNING ONCE: function "qat_hal_init_gpr" has inline asm
KLEE: WARNING ONCE: function "qat_hal_init_rd_xfer" has inline asm
KLEE: WARNING ONCE: function "qat_hal_init_wr_xfer" has inline asm
KLEE: WARNING ONCE: function "qat_hal_init_nn" has inline asm
KLEE: WARNING ONCE: function "qat_hal_clr_reset" has inline asm
KLEE: WARNING ONCE: function "adf_dev_start" has inline asm
KLEE: WARNING ONCE: function "qat_algs_register" has inline asm
KLEE: WARNING ONCE: function "adf_dev_stop" has inline asm
KLEE: WARNING ONCE: function "qat_algs_unregister" has inline asm
KLEE: WARNING ONCE: function "adf_dev_shutdown" has inline asm
KLEE: WARNING ONCE: function "adf_cfg_del_all" has inline asm
KLEE: WARNING ONCE: function "adf_response_handler" has inline asm
KLEE: WARNING ONCE: function "adf_ctl_ioctl" has inline asm
KLEE: WARNING ONCE: function "adf_slot_reset" has inline asm
KLEE: WARNING ONCE: function "adf_device_reset_worker" has inline asm
KLEE: WARNING ONCE: function "qat_alg_aead_setkey" has inline asm
KLEE: WARNING ONCE: function "qat_alg_aead_exit" has inline asm
KLEE: WARNING ONCE: function "qat_alg_ablkcipher_setkey" has inline asm
KLEE: WARNING ONCE: function "qat_alg_ablkcipher_exit" has inline asm
KLEE: WARNING ONCE: function "adf_dev_put" has inline asm
KLEE: WARNING ONCE: function "adf_send_message" has inline asm
KLEE: WARNING ONCE: function "dma_unmap_single_attrs" has inline asm
KLEE: WARNING ONCE: function "dma_map_single_attrs" has inline asm
KLEE: WARNING ONCE: function "sg_virt" has inline asm
KLEE: WARNING ONCE: function "qat_crypto_get_instance_node" has inline asm
KLEE: WARNING ONCE: function "adf_dev_get" has inline asm
KLEE: WARNING ONCE: function "adf_ring_show" has inline asm
KLEE: WARNING ONCE: function "adf_bank_show" has inline asm
KLEE: WARNING ONCE: function "qat_hal_reset" has inline asm
KLEE: WARNING ONCE: function "qat_crypto_put_instance" has inline asm
KLEE: WARNING ONCE: function "adf_create_ring" has inline asm
KLEE: WARNING ONCE: function "qat_crypto_free_instances" has inline asm
KLEE: WARNING ONCE: function "adf_remove_ring" has inline asm
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_5e5225ec-a40d-4f89-8622-ea230aef1d1b/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: killing 14523 states (over memory cap)
KLEE: WARNING: killing 15036 states (over memory cap)
KLEE: WARNING: killing 15309 states (over memory cap)
KLEE: WARNING: killing 14880 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 14377 states (over memory cap)
KLEE: WARNING: killing 14190 states (over memory cap)
KLEE: WARNING: killing 14392 states (over memory cap)
KLEE: WARNING: killing 13894 states (over memory cap)
KLEE: WARNING: killing 14484 states (over memory cap)
KLEE: WARNING: killing 14530 states (over memory cap)
KLEE: WARNING: killing 14887 states (over memory cap)
KLEE: WARNING: killing 15165 states (over memory cap)
KLEE: WARNING: killing 15298 states (over memory cap)
KLEE: WARNING: killing 16497 states (over memory cap)
KLEE: WARNING: killing 16246 states (over memory cap)
KLEE: WARNING: killing 16448 states (over memory cap)
KLEE: WARNING: killing 16738 states (over memory cap)
KLEE: WARNING: killing 16339 states (over memory cap)
KLEE: WARNING: killing 16314 states (over memory cap)
KLEE: WARNING: killing 16297 states (over memory cap)
KLEE: WARNING: killing 16508 states (over memory cap)
KLEE: WARNING: killing 16485 states (over memory cap)
KLEE: WARNING: killing 15333 states (over memory cap)
KLEE: WARNING: killing 15765 states (over memory cap)
KLEE: WARNING: killing 15819 states (over memory cap)
KLEE: WARNING: killing 15646 states (over memory cap)
KLEE: WARNING: killing 15178 states (over memory cap)
KLEE: WARNING: killing 15380 states (over memory cap)
KLEE: WARNING: killing 15137 states (over memory cap)
KLEE: WARNING: killing 15190 states (over memory cap)
KLEE: WARNING: killing 16222 states (over memory cap)
KLEE: WARNING: killing 15823 states (over memory cap)
KLEE: WARNING: killing 15726 states (over memory cap)
KLEE: WARNING: killing 15408 states (over memory cap)
KLEE: WARNING: killing 15241 states (over memory cap)
KLEE: WARNING: killing 16120 states (over memory cap)
KLEE: WARNING: killing 15655 states (over memory cap)
KLEE: WARNING: killing 15857 states (over memory cap)
KLEE: WARNING: killing 15095 states (over memory cap)
KLEE: WARNING: killing 16784 states (over memory cap)
KLEE: WARNING: killing 16177 states (over memory cap)
KLEE: WARNING: killing 15937 states (over memory cap)
KLEE: WARNING: killing 15924 states (over memory cap)
KLEE: WARNING: killing 15830 states (over memory cap)
KLEE: WARNING: killing 15153 states (over memory cap)
KLEE: WARNING: killing 15354 states (over memory cap)
KLEE: WARNING: killing 15776 states (over memory cap)
KLEE: WARNING: killing 15469 states (over memory cap)
KLEE: WARNING: killing 15378 states (over memory cap)
KLEE: WARNING: killing 15579 states (over memory cap)
KLEE: WARNING: killing 16004 states (over memory cap)
KLEE: WARNING: killing 16054 states (over memory cap)
KLEE: WARNING: killing 15385 states (over memory cap)
KLEE: WARNING: killing 15516 states (over memory cap)
KLEE: WARNING: killing 15500 states (over memory cap)
KLEE: WARNING: killing 15844 states (over memory cap)
KLEE: WARNING: killing 15468 states (over memory cap)
KLEE: WARNING: killing 15885 states (over memory cap)
KLEE: WARNING: killing 15580 states (over memory cap)
KLEE: WARNING: killing 15566 states (over memory cap)
KLEE: WARNING: killing 15836 states (over memory cap)
KLEE: WARNING: killing 15607 states (over memory cap)
KLEE: WARNING: killing 15517 states (over memory cap)
KLEE: WARNING: killing 15573 states (over memory cap)
KLEE: WARNING: killing 15843 states (over memory cap)
KLEE: WARNING: killing 15325 states (over memory cap)
KLEE: WARNING: killing 15526 states (over memory cap)
KLEE: WARNING: killing 15291 states (over memory cap)
KLEE: WARNING: killing 16142 states (over memory cap)
KLEE: WARNING: killing 15474 states (over memory cap)
KLEE: WARNING: killing 15820 states (over memory cap)
KLEE: WARNING: killing 15586 states (over memory cap)
KLEE: WARNING: killing 15641 states (over memory cap)
KLEE: WARNING: killing 16205 states (over memory cap)
KLEE: WARNING: killing 15620 states (over memory cap)
KLEE: WARNING: killing 15677 states (over memory cap)
KLEE: WARNING: killing 16166 states (over memory cap)
KLEE: WARNING: killing 15796 states (over memory cap)
KLEE: WARNING: killing 16281 states (over memory cap)
KLEE: WARNING: killing 15481 states (over memory cap)
KLEE: WARNING: killing 15532 states (over memory cap)
KLEE: WARNING: killing 15516 states (over memory cap)
KLEE: WARNING: killing 15640 states (over memory cap)
KLEE: WARNING: killing 16056 states (over memory cap)
KLEE: WARNING: killing 15254 states (over memory cap)
KLEE: WARNING: killing 15454 states (over memory cap)
KLEE: WARNING: killing 15863 states (over memory cap)
KLEE: WARNING: killing 15630 states (over memory cap)
KLEE: WARNING: killing 15334 states (over memory cap)
KLEE: WARNING: killing 15889 states (over memory cap)
KLEE: WARNING: killing 15658 states (over memory cap)
KLEE: WARNING: killing 15713 states (over memory cap)
KLEE: WARNING: killing 15695 states (over memory cap)
KLEE: WARNING: killing 15826 states (over memory cap)
KLEE: WARNING: killing 15889 states (over memory cap)
KLEE: WARNING: killing 15451 states (over memory cap)
KLEE: WARNING: killing 15925 states (over memory cap)
KLEE: WARNING: killing 16478 states (over memory cap)
KLEE: WARNING: killing 15127 states (over memory cap)
KLEE: WARNING: killing 15254 states (over memory cap)
KLEE: WARNING: killing 15374 states (over memory cap)
KLEE: WARNING: killing 15785 states (over memory cap)
KLEE: WARNING: killing 15485 states (over memory cap)
KLEE: WARNING: killing 15680 states (over memory cap)
KLEE: WARNING: killing 15944 states (over memory cap)
KLEE: WARNING: killing 15441 states (over memory cap)
KLEE: WARNING: killing 15635 states (over memory cap)
KLEE: WARNING: killing 15893 states (over memory cap)
KLEE: WARNING: killing 15886 states (over memory cap)
KLEE: WARNING: killing 16290 states (over memory cap)
KLEE: WARNING: killing 15645 states (over memory cap)
KLEE: WARNING: killing 15426 states (over memory cap)
KLEE: WARNING: killing 15408 states (over memory cap)
KLEE: WARNING: killing 15810 states (over memory cap)
KLEE: WARNING: killing 15725 states (over memory cap)
KLEE: WARNING: killing 15641 states (over memory cap)
KLEE: WARNING: killing 15905 states (over memory cap)
KLEE: WARNING: killing 15896 states (over memory cap)
KLEE: WARNING: killing 15195 states (over memory cap)
KLEE: WARNING: killing 15247 states (over memory cap)
KLEE: WARNING: killing 15923 states (over memory cap)
KLEE: WARNING: killing 15567 states (over memory cap)
KLEE: WARNING: killing 15280 states (over memory cap)
KLEE: WARNING: killing 16016 states (over memory cap)
KLEE: WARNING: killing 15112 states (over memory cap)
KLEE: WARNING: killing 15786 states (over memory cap)
KLEE: WARNING: killing 15837 states (over memory cap)
KLEE: WARNING: killing 15480 states (over memory cap)
KLEE: WARNING: killing 15675 states (over memory cap)
KLEE: WARNING: killing 16142 states (over memory cap)
KLEE: WARNING: killing 15991 states (over memory cap)
KLEE: WARNING: killing 15230 states (over memory cap)
KLEE: WARNING: killing 15691 states (over memory cap)
KLEE: WARNING: killing 16015 states (over memory cap)
KLEE: WARNING: killing 15938 states (over memory cap)
KLEE: WARNING: killing 15859 states (over memory cap)
KLEE: WARNING: killing 15774 states (over memory cap)
KLEE: WARNING: killing 15418 states (over memory cap)
KLEE: WARNING: killing 15407 states (over memory cap)
KLEE: WARNING: killing 15872 states (over memory cap)
KLEE: WARNING: killing 15318 states (over memory cap)
KLEE: WARNING: killing 15645 states (over memory cap)
KLEE: WARNING: killing 15627 states (over memory cap)
KLEE: WARNING: killing 15543 states (over memory cap)
KLEE: WARNING: killing 15123 states (over memory cap)
KLEE: WARNING: killing 15046 states (over memory cap)
KLEE: WARNING: killing 16174 states (over memory cap)
KLEE: WARNING: killing 15754 states (over memory cap)
KLEE: WARNING: killing 15947 states (over memory cap)
KLEE: WARNING: killing 15934 states (over memory cap)
KLEE: WARNING: killing 15990 states (over memory cap)
KLEE: WARNING: killing 15170 states (over memory cap)
KLEE: WARNING: killing 15224 states (over memory cap)
KLEE: WARNING: killing 15415 states (over memory cap)
KLEE: WARNING: killing 15604 states (over memory cap)
KLEE: WARNING: killing 15650 states (over memory cap)
KLEE: WARNING: killing 15639 states (over memory cap)
KLEE: WARNING: killing 15558 states (over memory cap)
KLEE: WARNING: killing 15613 states (over memory cap)
KLEE: WARNING: killing 15060 states (over memory cap)
KLEE: WARNING: killing 15243 states (over memory cap)
KLEE: WARNING: killing 15562 states (over memory cap)
KLEE: WARNING: killing 16419 states (over memory cap)
KLEE: WARNING: killing 15406 states (over memory cap)
KLEE: WARNING: killing 16060 states (over memory cap)
KLEE: WARNING: killing 15117 states (over memory cap)
KLEE: WARNING: killing 15168 states (over memory cap)
KLEE: WARNING: killing 15553 states (over memory cap)
KLEE: WARNING: killing 16332 states (over memory cap)
KLEE: WARNING: killing 15926 states (over memory cap)
KLEE: WARNING: killing 16246 states (over memory cap)
KLEE: WARNING: killing 15113 states (over memory cap)
KLEE: WARNING: killing 15823 states (over memory cap)
KLEE: WARNING: killing 15741 states (over memory cap)
KLEE: WARNING: killing 15460 states (over memory cap)
KLEE: WARNING: killing 15318 states (over memory cap)
KLEE: WARNING: killing 15560 states (over memory cap)
KLEE: WARNING: killing 14952 states (over memory cap)
KLEE: WARNING: killing 15595 states (over memory cap)
KLEE: WARNING: killing 15710 states (over memory cap)
KLEE: WARNING: killing 15303 states (over memory cap)
KLEE: WARNING: killing 16073 states (over memory cap)
KLEE: WARNING: killing 15936 states (over memory cap)
KLEE: WARNING: killing 15726 states (over memory cap)
KLEE: WARNING: killing 16239 states (over memory cap)
KLEE: WARNING: killing 15113 states (over memory cap)
KLEE: WARNING: killing 15289 states (over memory cap)
KLEE: WARNING: killing 15540 states (over memory cap)
