bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--video--aty--atyfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.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.: 179 138 2424 36385
INFO: Compilation, preparation and instrumentation time: 1.1685860157
Removed calls to '___udelay' (function is undefined)
Defining function printk as symbolic
Removed calls to 'iounmap' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'fb_dealloc_cmap' (function is undefined)
Removed calls to '__release_region' (function is undefined)
Removed calls to 'framebuffer_release' (function is undefined)
Removed calls to 'backlight_device_unregister' (function is undefined)
Removed calls to 'console_lock' (function is undefined)
Removed calls to 'fb_set_suspend' (function is undefined)
Removed calls to 'console_unlock' (function is undefined)
Defining function dev_get_drvdata as symbolic
Defining function pci_save_state as symbolic
Defining function pci_choose_state as symbolic
Defining function pci_set_power_state as symbolic
Defining function unregister_framebuffer as symbolic
Defining function mtrr_del as symbolic
Defining function pci_enable_device as symbolic
Defining function __request_region as symbolic
Defining function framebuffer_alloc as symbolic
Defining function mtrr_add as symbolic
Defining function fb_find_mode as symbolic
Defining function fb_alloc_cmap as symbolic
Defining function register_framebuffer as symbolic
Defining function dev_set_drvdata as symbolic
Defining function pci_bus_write_config_word as symbolic
Defining function pci_bus_read_config_word as symbolic
Defining function ioremap_nocache as symbolic
Defining function lock_fb_info as symbolic
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'cfb_fillrect' (function is undefined)
Removed calls to 'cfb_copyarea' (function is undefined)
Removed calls to 'cfb_imageblit' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'prepare_to_wait' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Defining function autoremove_wake_function as symbolic
Defining function schedule_timeout as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function request_threaded_irq as symbolic
Defining function __pci_register_driver as symbolic
Defining function dmi_check_system as symbolic
Defining function register_reboot_notifier as symbolic
Removed calls to 'pci_unregister_driver' (function is undefined)
Defining function unregister_reboot_notifier as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'ldv_check_return_value' (function is undefined)
Linked our definitions to these undefined functions:
  __memcpy
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 0.853756189346
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 291 107 965 19805
INFO: Starting verification
KLEE: WARNING ONCE: function "aty_set_dac_514" has inline asm
KLEE: WARNING ONCE: function "aty_set_pll_514" has inline asm
KLEE: WARNING ONCE: function "aty_set_dac_ATI68860_B" has inline asm
KLEE: WARNING ONCE: function "aty_set_dac_ATT21C498" has inline asm
KLEE: WARNING ONCE: function "aty_set_pll18818" has inline asm
KLEE: WARNING ONCE: function "aty_StrobeClock" has inline asm
KLEE: WARNING ONCE: function "aty_ICS2595_put1bit" has inline asm
KLEE: WARNING ONCE: function "aty_set_pll_1703" has inline asm
KLEE: WARNING ONCE: function "aty_set_pll_8398" has inline asm
KLEE: WARNING ONCE: function "aty_set_pll_408" has inline asm
KLEE: WARNING ONCE: function "aty_set_dac_unsupported" has inline asm
KLEE: WARNING ONCE: function "aty_set_pll_ct" has inline asm
KLEE: WARNING ONCE: function "aty_get_pll_ct" has inline asm
KLEE: WARNING ONCE: function "aty_init_pll_ct" has inline asm
KLEE: WARNING ONCE: function "aty_resume_pll_ct" has inline asm
KLEE: WARNING ONCE: function "aty_ld_lcd" has inline asm
KLEE: WARNING ONCE: function "aty_st_lcd" has inline asm
KLEE: WARNING ONCE: function "atyfb_pci_probe" has inline asm
KLEE: WARNING ONCE: function "atyfb_pci_resume" has inline asm
KLEE: WARNING ONCE: function "atyfb_set_par" has inline asm
KLEE: WARNING ONCE: function "atyfb_blank" has inline asm
KLEE: WARNING ONCE: function "aty_var_to_crtc" has inline asm
KLEE: WARNING ONCE: function "wait_for_idle" has inline asm
KLEE: WARNING ONCE: function "aty_set_crtc" has inline asm
KLEE: WARNING ONCE: function "aty_init_engine" has inline asm
KLEE: WARNING ONCE: function "aty_reset_engine" has inline asm
KLEE: WARNING ONCE: function "atyfb_cursor" has inline asm
KLEE: WARNING ONCE: function "atyfb_release" has inline asm
KLEE: WARNING ONCE: function "atyfb_setcolreg" has inline asm
KLEE: WARNING ONCE: function "atyfb_pan_display" has inline asm
KLEE: WARNING ONCE: function "atyfb_fillrect" has inline asm
KLEE: WARNING ONCE: function "atyfb_copyarea" has inline asm
KLEE: WARNING ONCE: function "atyfb_imageblit" has inline asm
KLEE: WARNING ONCE: function "atyfb_ioctl" has inline asm
KLEE: WARNING ONCE: function "aty_enable_irq" has inline asm
KLEE: WARNING ONCE: function "aty_irq" has inline asm
KLEE: WARNING ONCE: function "draw_rect" has inline asm
KLEE: WARNING ONCE: function "aty_ld_pll_ct" has inline asm
KLEE: WARNING ONCE: function "ldv_main3_sequence_infinite_withcheck_stateful" has inline asm
KLEE: WARNING ONCE: flushing 6568 bytes on read, may be slow and/or crash: MO190[6568] allocated at global:
KLEE: ERROR: /tmp/symbiotic-wBHLBf/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--video--aty--atyfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:9967: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wBHLBf/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--video--aty--atyfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:9465: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wBHLBf/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--video--aty--atyfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:4694: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wBHLBf/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--video--aty--atyfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:12882: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wBHLBf/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--video--aty--atyfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:12886: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wBHLBf/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--video--aty--atyfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:8487: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wBHLBf/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--video--aty--atyfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:13564: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wBHLBf/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--video--aty--atyfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:9477: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wBHLBf/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--video--aty--atyfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:9112: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wBHLBf/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--video--aty--atyfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:13575: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wBHLBf/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--video--aty--atyfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:12638: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wBHLBf/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--video--aty--atyfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:4699: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wBHLBf/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--video--aty--atyfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:9972: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wBHLBf/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--video--aty--atyfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:12891: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wBHLBf/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--video--aty--atyfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:8495: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wBHLBf/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--video--aty--atyfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:4450: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wBHLBf/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--video--aty--atyfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:9119: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wBHLBf/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--video--aty--atyfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:9574: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wBHLBf/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--video--aty--atyfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:12643: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wBHLBf/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--video--aty--atyfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:4450: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wBHLBf/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--video--aty--atyfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:10170: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wBHLBf/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--video--aty--atyfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:13615: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wBHLBf/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--video--aty--atyfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:10010: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wBHLBf/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--video--aty--atyfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:4061: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wBHLBf/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--video--aty--atyfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:4450: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wBHLBf/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--video--aty--atyfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:12912: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wBHLBf/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--video--aty--atyfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:4061: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
