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--media--pci--pt3--earth-pt3.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.: 91 102 937 5271
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 0.28072309494
Removed calls to 'dev_warn' (function is undefined)
Removed calls to 'iowrite32' (function is undefined)
Removed calls to 'usleep_range' (function is undefined)
Defining function ioread32 as symbolic
Removed calls to 'pci_set_master' (function is undefined)
Removed calls to '_dev_info' (function is undefined)
Removed calls to 'dev_err' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'i2c_unregister_device' (function is undefined)
Removed calls to 'dvb_dmxdev_release' (function is undefined)
Removed calls to 'dvb_dmx_release' (function is undefined)
Removed calls to 'i2c_del_adapter' (function is undefined)
Removed calls to 'pci_iounmap' (function is undefined)
Removed calls to 'pci_release_regions' (function is undefined)
Removed calls to 'pci_disable_device' (function is undefined)
Defining function dvb_unregister_frontend as symbolic
Removed calls to 'dma_free_attrs' (function is undefined)
Defining function dvb_unregister_adapter as symbolic
Removed calls to 'msleep' (function is undefined)
Defining function kthread_stop as symbolic
Defining function pci_enable_device as symbolic
Defining function pci_request_regions as symbolic
Defining function dma_set_mask as symbolic
Defining function pci_ioremap_bar as symbolic
Defining function strlcpy as symbolic
Defining function i2c_add_adapter as symbolic
Removed calls to 'mutex_unlock' (function is undefined)
Defining function mutex_lock_interruptible_nested as symbolic
Defining function i2c_transfer as symbolic
Defining function __request_module as symbolic
Defining function i2c_new_device as symbolic
Defining function dvb_register_frontend as symbolic
Defining function dvb_register_adapter as symbolic
Defining function dvb_dmx_init as symbolic
Defining function dvb_dmxdev_init as symbolic
Defining function dma_alloc_attrs as symbolic
Removed calls to 'debug_check_no_locks_held' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Defining function kthread_create_on_node as symbolic
Defining function wake_up_process as symbolic
Defining function set_freezable as symbolic
Removed calls to 'dvb_dmx_swfilter_packets' (function is undefined)
Defining function kthread_freezable_should_stop as symbolic
Defining function schedule_hrtimeout_range as symbolic
Defining function __refrigerator as symbolic
Defining function freezing_slow_path as symbolic
Defining function dma_supported as symbolic
Defining function pci_bus_read_config_byte as symbolic
Defining function dvb_frontend_resume as symbolic
Defining function dvb_frontend_suspend as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'pci_unregister_driver' (function is undefined)
Defining function ldv_shutdown_1 as symbolic
Defining function ldv_suspend_late_2 as symbolic
Defining function ldv_restore_early_2 as symbolic
Defining function ldv_resume_early_2 as symbolic
Defining function ldv_thaw_early_2 as symbolic
Defining function ldv_resume_noirq_2 as symbolic
Defining function ldv_freeze_noirq_2 as symbolic
Defining function ldv_prepare_2 as symbolic
Defining function ldv_freeze_late_2 as symbolic
Defining function ldv_thaw_noirq_2 as symbolic
Defining function ldv_poweroff_noirq_2 as symbolic
Defining function ldv_poweroff_late_2 as symbolic
Defining function ldv_restore_noirq_2 as symbolic
Defining function ldv_suspend_noirq_2 as symbolic
Defining function ldv_complete_2 as symbolic
Defining function __pci_register_driver as symbolic
Linked our definitions to these undefined functions:
  strncmp
  __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.297986030579
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 133 116 571 3032
INFO: Starting verification
KLEE: WARNING ONCE: function "pt3_start_feed" has inline asm
KLEE: WARNING ONCE: function "pt3_fetch_thread" 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_c0f2d317-5a64-4345-ba51-e3ddbad2a05a/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-o6IMD6/linux-4.2-rc1.tar.xz-08_1a-drivers--media--pci--pt3--earth-pt3.ko-entry_point_false-unreach-call.cil.out.c:6900: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-o6IMD6/linux-4.2-rc1.tar.xz-08_1a-drivers--media--pci--pt3--earth-pt3.ko-entry_point_false-unreach-call.cil.out.c:5719: 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 13048 states (over memory cap)
KLEE: WARNING: killing 11936 states (over memory cap)
KLEE: WARNING: killing 11985 states (over memory cap)
KLEE: WARNING: killing 12427 states (over memory cap)
KLEE: WARNING: killing 12585 states (over memory cap)
KLEE: WARNING: killing 12733 states (over memory cap)
KLEE: WARNING: killing 12881 states (over memory cap)
KLEE: WARNING: killing 12945 states (over memory cap)
KLEE: WARNING: killing 13095 states (over memory cap)
KLEE: WARNING: killing 13344 states (over memory cap)
KLEE: WARNING: killing 13122 states (over memory cap)
KLEE: WARNING: killing 13183 states (over memory cap)
KLEE: WARNING: killing 13052 states (over memory cap)
KLEE: WARNING: killing 13481 states (over memory cap)
KLEE: WARNING: killing 14013 states (over memory cap)
KLEE: WARNING: killing 14544 states (over memory cap)
KLEE: WARNING: killing 14415 states (over memory cap)
KLEE: WARNING: killing 14290 states (over memory cap)
KLEE: WARNING: killing 13600 states (over memory cap)
KLEE: WARNING: killing 14217 states (over memory cap)
KLEE: WARNING: killing 13904 states (over memory cap)
KLEE: WARNING: killing 14416 states (over memory cap)
KLEE: WARNING: killing 14653 states (over memory cap)
KLEE: WARNING: killing 14162 states (over memory cap)
KLEE: WARNING: killing 14036 states (over memory cap)
KLEE: WARNING: killing 14087 states (over memory cap)
KLEE: WARNING: killing 14959 states (over memory cap)
KLEE: WARNING: killing 14560 states (over memory cap)
KLEE: WARNING: killing 14164 states (over memory cap)
KLEE: WARNING: killing 14587 states (over memory cap)
KLEE: WARNING: killing 14102 states (over memory cap)
KLEE: WARNING: killing 14695 states (over memory cap)
KLEE: WARNING: killing 14752 states (over memory cap)
KLEE: WARNING: killing 15168 states (over memory cap)
KLEE: WARNING: killing 14955 states (over memory cap)
KLEE: WARNING: killing 14919 states (over memory cap)
KLEE: WARNING: killing 15253 states (over memory cap)
KLEE: WARNING: killing 13973 states (over memory cap)
KLEE: WARNING: killing 15006 states (over memory cap)
KLEE: WARNING: killing 15152 states (over memory cap)
KLEE: WARNING: killing 14591 states (over memory cap)
KLEE: WARNING: killing 14373 states (over memory cap)
KLEE: WARNING: killing 14960 states (over memory cap)
KLEE: WARNING: killing 14748 states (over memory cap)
KLEE: WARNING: killing 15149 states (over memory cap)
KLEE: WARNING: killing 14854 states (over memory cap)
KLEE: WARNING: killing 15171 states (over memory cap)
KLEE: WARNING: killing 14885 states (over memory cap)
KLEE: WARNING: killing 15375 states (over memory cap)
KLEE: WARNING: killing 15000 states (over memory cap)
KLEE: WARNING: killing 15051 states (over memory cap)
KLEE: WARNING: killing 15282 states (over memory cap)
KLEE: WARNING: killing 15000 states (over memory cap)
KLEE: WARNING: killing 14620 states (over memory cap)
KLEE: WARNING: killing 14507 states (over memory cap)
KLEE: WARNING: killing 14814 states (over memory cap)
KLEE: WARNING: killing 15035 states (over memory cap)
KLEE: WARNING: killing 15181 states (over memory cap)
KLEE: WARNING: killing 15146 states (over memory cap)
KLEE: WARNING: killing 14772 states (over memory cap)
KLEE: WARNING: killing 15085 states (over memory cap)
KLEE: WARNING: killing 14622 states (over memory cap)
KLEE: WARNING: killing 14934 states (over memory cap)
KLEE: WARNING: killing 14828 states (over memory cap)
KLEE: WARNING: killing 8377 states (over memory cap)
KLEE: WARNING: killing 13954 states (over memory cap)
KLEE: WARNING: killing 15093 states (over memory cap)
KLEE: WARNING: killing 14904 states (over memory cap)
KLEE: WARNING: killing 14959 states (over memory cap)
KLEE: WARNING: killing 15103 states (over memory cap)
KLEE: WARNING: killing 14571 states (over memory cap)
KLEE: WARNING: killing 8362 states (over memory cap)
KLEE: WARNING: killing 14614 states (over memory cap)
KLEE: WARNING: killing 14916 states (over memory cap)
KLEE: WARNING: killing 14481 states (over memory cap)
KLEE: WARNING: killing 8389 states (over memory cap)
KLEE: WARNING: killing 14608 states (over memory cap)
KLEE: WARNING: killing 15241 states (over memory cap)
KLEE: WARNING: killing 8351 states (over memory cap)
KLEE: WARNING: killing 14625 states (over memory cap)
KLEE: WARNING: killing 15004 states (over memory cap)
KLEE: WARNING: killing 8233 states (over memory cap)
KLEE: WARNING: killing 14154 states (over memory cap)
KLEE: WARNING: killing 14609 states (over memory cap)
KLEE: WARNING: killing 14503 states (over memory cap)
KLEE: WARNING: killing 8097 states (over memory cap)
KLEE: WARNING: killing 14546 states (over memory cap)
KLEE: WARNING: killing 8317 states (over memory cap)
KLEE: WARNING: killing 14183 states (over memory cap)
KLEE: WARNING: killing 8292 states (over memory cap)
KLEE: WARNING: killing 14222 states (over memory cap)
KLEE: WARNING: killing 8349 states (over memory cap)
KLEE: WARNING: killing 14506 states (over memory cap)
KLEE: WARNING: killing 8009 states (over memory cap)
KLEE: WARNING: killing 14467 states (over memory cap)
KLEE: WARNING: killing 8228 states (over memory cap)
KLEE: WARNING: killing 14512 states (over memory cap)
KLEE: WARNING: killing 8607 states (over memory cap)
KLEE: WARNING: killing 13998 states (over memory cap)
KLEE: WARNING: killing 14846 states (over memory cap)
KLEE: WARNING: killing 8011 states (over memory cap)
KLEE: WARNING: killing 13772 states (over memory cap)
KLEE: WARNING: killing 8065 states (over memory cap)
KLEE: WARNING: killing 13890 states (over memory cap)
KLEE: WARNING: killing 8121 states (over memory cap)
KLEE: WARNING: killing 14007 states (over memory cap)
KLEE: WARNING: killing 8334 states (over memory cap)
KLEE: WARNING: killing 14529 states (over memory cap)
KLEE: WARNING: killing 8472 states (over memory cap)
KLEE: WARNING: killing 14261 states (over memory cap)
KLEE: WARNING: killing 8061 states (over memory cap)
KLEE: WARNING: killing 14460 states (over memory cap)
KLEE: WARNING: killing 7959 states (over memory cap)
KLEE: WARNING: killing 14024 states (over memory cap)
KLEE: WARNING: killing 8328 states (over memory cap)
KLEE: WARNING: killing 14377 states (over memory cap)
KLEE: WARNING: killing 7994 states (over memory cap)
KLEE: WARNING: killing 14341 states (over memory cap)
KLEE: WARNING: killing 8286 states (over memory cap)
KLEE: WARNING: killing 14000 states (over memory cap)
KLEE: WARNING: killing 8340 states (over memory cap)
KLEE: WARNING: killing 13969 states (over memory cap)
KLEE: WARNING: killing 8246 states (over memory cap)
KLEE: WARNING: killing 7706 states (over memory cap)
KLEE: WARNING: killing 14083 states (over memory cap)
