bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--parport--parport_pc.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.: 228 182 1771 11070
Removed infinite loop in dma_map_single_attrs
Removed infinite loop in dma_unmap_single_attrs
Removed infinite loop in arch_local_save_flags
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.440671920776
Removed calls to 'platform_device_unregister' (function is undefined)
Defining function dev_err as symbolic
Defining function __request_region as symbolic
Defining function printk as symbolic
Defining function parport_irq_handler as symbolic
Defining function parport_ieee1284_ecp_write_data as symbolic
Defining function parport_ieee1284_write_compat as symbolic
Defining function dma_set_mask as symbolic
Defining function dma_supported as symbolic
Defining function platform_device_register_full as symbolic
Removed calls to 'parport_remove_port' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'free_dma' (function is undefined)
Removed calls to 'free_irq' (function is undefined)
Removed calls to '__release_region' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'debug_dma_free_coherent' (function is undefined)
Removed calls to 'parport_put_port' (function is undefined)
Defining function parport_ieee1284_epp_write_data as symbolic
Defining function parport_ieee1284_epp_read_data as symbolic
Defining function parport_ieee1284_epp_write_addr as symbolic
Defining function parport_ieee1284_epp_read_addr as symbolic
Defining function parport_ieee1284_ecp_read_data as symbolic
Defining function parport_ieee1284_ecp_write_addr as symbolic
Defining function parport_ieee1284_read_nibble as symbolic
Defining function parport_ieee1284_read_byte as symbolic
Defining function pci_enable_device as symbolic
Defining function _dev_info as symbolic
Defining function pnp_get_resource as symbolic
Defining function pci_bus_read_config_dword as symbolic
Defining function pci_bus_read_config_byte as symbolic
Defining function pci_bus_write_config_dword as symbolic
Defining function pci_bus_write_config_byte as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'pci_unregister_driver' (function is undefined)
Removed calls to 'pnp_unregister_driver' (function is undefined)
Removed calls to 'platform_driver_unregister' (function is undefined)
Removed calls to 'ldv_check_final_state' (function is undefined)
Defining function ldv_release_2 as symbolic
Defining function ldv_release_5 as symbolic
Defining function ldv_probe_5 as symbolic
Defining function pnp_register_driver as symbolic
Defining function __pci_register_driver as symbolic
Defining function pci_match_id as symbolic
Defining function pci_get_device as symbolic
Defining function __platform_driver_register as symbolic
Defining function kmem_cache_alloc as symbolic
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  strcmp
  strncmp
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_assume
  __VERIFIER_calloc0
  __VERIFIER_error
  __VERIFIER_exit
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
  __VERIFIER_nondet_pointer_named
  __VERIFIER_nondet_size_t_named
  __VERIFIER_nondet_uchar_named
  __VERIFIER_nondet_ulong_named
INFO: After-slicing optimizations and preparation time: 0.325258016586
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 217 93 444 3075
INFO: Starting verification
KLEE: WARNING ONCE: function "parport_pc_unregister_port" has inline asm
KLEE: WARNING ONCE: function "sio_via_probe" has inline asm
KLEE: WARNING ONCE: function "sio_ite_8872_probe" has inline asm
KLEE: WARNING ONCE: function "main" has inline asm
KLEE: WARNING ONCE: function "winbond_check" has inline asm
KLEE: WARNING ONCE: function "winbond_check2" has inline asm
KLEE: WARNING ONCE: function "smsc_check" has inline asm
KLEE: WARNING ONCE: function "parport_pc_restore_state" has inline asm
KLEE: WARNING ONCE: function "parport_pc_frob_control" has inline asm
KLEE: WARNING ONCE: function "parport_pc_write_control" has inline asm
KLEE: WARNING ONCE: function "decode_winbond" 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_d50097ea-b9cd-4779-a63b-ac2b60059357/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2HoSno/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--parport--parport_pc.ko-entry_point_true-unreach-call.cil.out.c:4024: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 6094 states (over memory cap)
KLEE: WARNING: killing 5264 states (over memory cap)
KLEE: WARNING: killing 5345 states (over memory cap)
KLEE: WARNING: killing 5514 states (over memory cap)
KLEE: WARNING: killing 6333 states (over memory cap)
KLEE: WARNING: killing 6199 states (over memory cap)
KLEE: WARNING: killing 6457 states (over memory cap)
KLEE: WARNING: killing 6499 states (over memory cap)
KLEE: WARNING: killing 6536 states (over memory cap)
KLEE: WARNING: killing 7095 states (over memory cap)
KLEE: WARNING: killing 7480 states (over memory cap)
KLEE: WARNING: killing 7692 states (over memory cap)
KLEE: WARNING: killing 8119 states (over memory cap)
KLEE: WARNING: killing 8202 states (over memory cap)
KLEE: WARNING: killing 8801 states (over memory cap)
KLEE: WARNING: killing 8534 states (over memory cap)
KLEE: WARNING: killing 9176 states (over memory cap)
KLEE: WARNING: killing 9126 states (over memory cap)
KLEE: WARNING: killing 9158 states (over memory cap)
KLEE: WARNING: killing 9366 states (over memory cap)
KLEE: WARNING: killing 9314 states (over memory cap)
KLEE: WARNING: killing 9304 states (over memory cap)
KLEE: WARNING: killing 9252 states (over memory cap)
KLEE: WARNING: killing 9244 states (over memory cap)
KLEE: WARNING: killing 8891 states (over memory cap)
KLEE: WARNING: killing 9178 states (over memory cap)
KLEE: WARNING: killing 9337 states (over memory cap)
KLEE: WARNING: killing 9328 states (over memory cap)
KLEE: WARNING: killing 9444 states (over memory cap)
KLEE: WARNING: killing 9350 states (over memory cap)
KLEE: WARNING: killing 9041 states (over memory cap)
KLEE: WARNING: killing 9580 states (over memory cap)
KLEE: WARNING: killing 9276 states (over memory cap)
KLEE: WARNING: killing 9011 states (over memory cap)
KLEE: WARNING: killing 9126 states (over memory cap)
KLEE: WARNING: killing 9245 states (over memory cap)
KLEE: WARNING: killing 9193 states (over memory cap)
KLEE: WARNING: killing 9182 states (over memory cap)
KLEE: WARNING: killing 9678 states (over memory cap)
KLEE: WARNING: killing 9416 states (over memory cap)
KLEE: WARNING: killing 9323 states (over memory cap)
KLEE: WARNING: killing 9608 states (over memory cap)
KLEE: WARNING: killing 9096 states (over memory cap)
KLEE: WARNING: killing 9000 states (over memory cap)
KLEE: WARNING: killing 9160 states (over memory cap)
KLEE: WARNING: killing 9233 states (over memory cap)
KLEE: WARNING: killing 9264 states (over memory cap)
KLEE: WARNING: killing 9592 states (over memory cap)
KLEE: WARNING: killing 9165 states (over memory cap)
KLEE: WARNING: killing 9073 states (over memory cap)
KLEE: WARNING: killing 9191 states (over memory cap)
KLEE: WARNING: killing 9432 states (over memory cap)
KLEE: WARNING: killing 9426 states (over memory cap)
KLEE: WARNING: killing 9209 states (over memory cap)
KLEE: WARNING: killing 9445 states (over memory cap)
KLEE: WARNING: killing 9356 states (over memory cap)
KLEE: WARNING: killing 9391 states (over memory cap)
KLEE: WARNING: killing 9380 states (over memory cap)
KLEE: WARNING: killing 8959 states (over memory cap)
KLEE: WARNING: killing 8744 states (over memory cap)
KLEE: WARNING: killing 9228 states (over memory cap)
KLEE: WARNING: killing 9428 states (over memory cap)
KLEE: WARNING: killing 8720 states (over memory cap)
KLEE: WARNING: killing 9538 states (over memory cap)
KLEE: WARNING: killing 9279 states (over memory cap)
KLEE: WARNING: killing 9151 states (over memory cap)
KLEE: WARNING: killing 9264 states (over memory cap)
KLEE: WARNING: killing 9297 states (over memory cap)
KLEE: WARNING: killing 9253 states (over memory cap)
KLEE: WARNING: killing 9326 states (over memory cap)
KLEE: WARNING: killing 8946 states (over memory cap)
KLEE: WARNING: killing 9142 states (over memory cap)
KLEE: WARNING: killing 9134 states (over memory cap)
KLEE: WARNING: killing 9577 states (over memory cap)
KLEE: WARNING: killing 9078 states (over memory cap)
KLEE: WARNING: killing 9073 states (over memory cap)
KLEE: WARNING: killing 9351 states (over memory cap)
KLEE: WARNING: killing 9135 states (over memory cap)
KLEE: WARNING: killing 9207 states (over memory cap)
KLEE: WARNING: killing 9283 states (over memory cap)
KLEE: WARNING: killing 9275 states (over memory cap)
KLEE: WARNING: killing 9394 states (over memory cap)
KLEE: WARNING: killing 9264 states (over memory cap)
KLEE: WARNING: killing 9013 states (over memory cap)
KLEE: WARNING: killing 9209 states (over memory cap)
KLEE: WARNING: killing 9360 states (over memory cap)
KLEE: WARNING: killing 9073 states (over memory cap)
KLEE: WARNING: killing 9146 states (over memory cap)
KLEE: WARNING: killing 9664 states (over memory cap)
KLEE: WARNING: killing 9092 states (over memory cap)
KLEE: WARNING: killing 9167 states (over memory cap)
KLEE: WARNING: killing 8954 states (over memory cap)
KLEE: WARNING: killing 9311 states (over memory cap)
KLEE: WARNING: killing 9306 states (over memory cap)
KLEE: WARNING: killing 9380 states (over memory cap)
KLEE: WARNING: killing 9293 states (over memory cap)
KLEE: WARNING: killing 9123 states (over memory cap)
KLEE: WARNING: killing 9439 states (over memory cap)
KLEE: WARNING: killing 9108 states (over memory cap)
KLEE: WARNING: killing 9264 states (over memory cap)
KLEE: WARNING: killing 9257 states (over memory cap)
KLEE: WARNING: killing 9007 states (over memory cap)
KLEE: WARNING: killing 9118 states (over memory cap)
KLEE: WARNING: killing 9390 states (over memory cap)
KLEE: WARNING: killing 9263 states (over memory cap)
KLEE: WARNING: killing 9254 states (over memory cap)
KLEE: WARNING: killing 9049 states (over memory cap)
KLEE: WARNING: killing 9601 states (over memory cap)
KLEE: WARNING: killing 9274 states (over memory cap)
KLEE: WARNING: killing 9190 states (over memory cap)
KLEE: WARNING: killing 9262 states (over memory cap)
KLEE: WARNING: killing 9414 states (over memory cap)
KLEE: WARNING: killing 9408 states (over memory cap)
KLEE: WARNING: killing 9436 states (over memory cap)
KLEE: WARNING: killing 9113 states (over memory cap)
KLEE: WARNING: killing 9385 states (over memory cap)
KLEE: WARNING: killing 9218 states (over memory cap)
KLEE: WARNING: killing 9133 states (over memory cap)
KLEE: WARNING: killing 8963 states (over memory cap)
KLEE: WARNING: killing 8997 states (over memory cap)
KLEE: WARNING: killing 9226 states (over memory cap)
KLEE: WARNING: killing 9182 states (over memory cap)
KLEE: WARNING: killing 9451 states (over memory cap)
KLEE: WARNING: killing 9483 states (over memory cap)
KLEE: WARNING: killing 9279 states (over memory cap)
KLEE: WARNING: killing 9194 states (over memory cap)
KLEE: WARNING: killing 8910 states (over memory cap)
KLEE: WARNING: killing 9455 states (over memory cap)
KLEE: WARNING: killing 9094 states (over memory cap)
KLEE: WARNING: killing 9441 states (over memory cap)
KLEE: WARNING: killing 9511 states (over memory cap)
KLEE: WARNING: killing 9310 states (over memory cap)
KLEE: WARNING: killing 9380 states (over memory cap)
KLEE: WARNING: killing 9137 states (over memory cap)
KLEE: WARNING: killing 9564 states (over memory cap)
KLEE: WARNING: killing 9320 states (over memory cap)
KLEE: WARNING: killing 9590 states (over memory cap)
KLEE: WARNING: killing 9307 states (over memory cap)
KLEE: WARNING: killing 8914 states (over memory cap)
KLEE: WARNING: killing 8864 states (over memory cap)
KLEE: WARNING: killing 9207 states (over memory cap)
KLEE: WARNING: killing 8967 states (over memory cap)
KLEE: WARNING: killing 9428 states (over memory cap)
KLEE: WARNING: killing 9266 states (over memory cap)
KLEE: WARNING: killing 9333 states (over memory cap)
KLEE: WARNING: killing 8825 states (over memory cap)
KLEE: WARNING: killing 9516 states (over memory cap)
KLEE: WARNING: killing 9394 states (over memory cap)
KLEE: WARNING: killing 9308 states (over memory cap)
