bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--video--via--viafb.ko-ldv_main12_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.: 259 650 4029 25843
Removed infinite loop in arch_local_save_flags
INFO: Compilation, preparation and instrumentation time: 0.920214891434
Removed calls to 'fb_dealloc_cmap' (function is undefined)
Removed calls to 'framebuffer_release' (function is undefined)
Defining function framebuffer_alloc as symbolic
Defining function printk as symbolic
Defining function fb_get_color_depth as symbolic
Defining function fb_alloc_cmap as symbolic
Defining function register_framebuffer as symbolic
Removed calls to '__list_add' (function is undefined)
Defining function unregister_framebuffer as symbolic
Removed calls to 'list_del' (function is undefined)
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function proc_mkdir as symbolic
Defining function proc_create_data as symbolic
Defining function i2c_transfer as symbolic
Removed calls to 'fb_edid_to_monspecs' (function is undefined)
Removed calls to 'fb_destroy_modedb' (function is undefined)
Defining function seq_lseek as symbolic
Defining function seq_read as symbolic
Defining function single_release as symbolic
Defining function single_open as symbolic
Defining function seq_printf as symbolic
Removed calls to 'might_fault' (function is undefined)
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Defining function strsep as symbolic
Defining function kstrtou8 as symbolic
Defining function _copy_from_user as symbolic
Defining function kstrtou8_from_user as symbolic
Defining function seq_putc as symbolic
Defining function seq_puts as symbolic
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)
Removed calls to '__udelay' (function is undefined)
Removed calls to '__const_udelay' (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)
Defining function memdup_user as symbolic
Removed calls to 'iounmap' (function is undefined)
Defining function ioremap_nocache as symbolic
Defining function _copy_to_user as symbolic
Defining function i2c_del_adapter as symbolic
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function sprintf as symbolic
Defining function i2c_bit_add_bus as symbolic
Defining function _raw_spin_lock_irqsave as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'pci_dev_put' (function is undefined)
Removed calls to 'iowrite32' (function is undefined)
Removed calls to 'platform_device_put' (function is undefined)
Removed calls to 'pci_disable_device' (function is undefined)
Removed calls to 'pci_restore_state' (function is undefined)
Removed calls to 'pci_set_master' (function is undefined)
Defining function pci_set_power_state as symbolic
Defining function pci_enable_device as symbolic
Defining function pci_save_state as symbolic
Defining function pci_choose_state as symbolic
Removed calls to 'platform_device_unregister' (function is undefined)
Removed calls to 'remove_proc_entry' (function is undefined)
Defining function platform_device_alloc as symbolic
Defining function dev_err as symbolic
Defining function platform_device_add as symbolic
Defining function ioremap_wc as symbolic
Defining function pci_get_device as symbolic
Defining function pci_bus_read_config_dword as symbolic
Defining function gpiochip_remove as symbolic
Defining function gpiochip_add as symbolic
Removed calls to 'ldv_handler_precall' (function is undefined)
Removed calls to 'ldv_check_return_value' (function is undefined)
Defining function mutex_trylock as symbolic
Defining function platform_driver_register as symbolic
Removed calls to 'platform_driver_unregister' (function is undefined)
Removed calls to 'ldv_check_return_value_probe' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to 'complete' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function request_threaded_irq as symbolic
Defining function ioread32 as symbolic
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'debug_dma_alloc_coherent' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'msleep' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'debug_dma_free_coherent' (function is undefined)
Defining function sg_next as symbolic
Defining function wait_for_completion_timeout as symbolic
Removed calls to 'pci_unregister_driver' (function is undefined)
Defining function __pci_register_driver as symbolic
Linked our definitions to these undefined functions:
  memcmp
  strcmp
  strcpy
  strlen
  strncmp
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 1.00730013847
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 407 581 2722 20441
INFO: Starting verification
KLEE: WARNING ONCE: function "viafb_init_chip_info" has inline asm
KLEE: WARNING ONCE: function "viafb_init_dac" has inline asm
KLEE: WARNING ONCE: function "hw_bitblt_1" has inline asm
KLEE: WARNING ONCE: function "hw_bitblt_2" has inline asm
KLEE: WARNING ONCE: function "viafb_reset_engine" has inline asm
KLEE: WARNING ONCE: function "viafb_set_bpp" has inline asm
KLEE: WARNING ONCE: function "viafb_tmds_trasmitter_identify" has inline asm
KLEE: WARNING ONCE: function "viafb_init_lcd_size" has inline asm
KLEE: WARNING ONCE: function "viafb_dvi_sense" has inline asm
KLEE: WARNING ONCE: function "cle266_set_primary_pll" has inline asm
KLEE: WARNING ONCE: function "cle266_set_secondary_pll" has inline asm
KLEE: WARNING ONCE: function "set_primary_clock_state" has inline asm
KLEE: WARNING ONCE: function "set_primary_clock_source" has inline asm
KLEE: WARNING ONCE: function "set_primary_pll_state" has inline asm
KLEE: WARNING ONCE: function "set_secondary_clock_state" has inline asm
KLEE: WARNING ONCE: function "set_secondary_clock_source" has inline asm
KLEE: WARNING ONCE: function "set_secondary_pll_state" has inline asm
KLEE: WARNING ONCE: function "set_engine_pll_state" has inline asm
KLEE: WARNING ONCE: function "set_engine_pll_encoded" has inline asm
KLEE: WARNING ONCE: function "k800_set_secondary_pll_encoded" has inline asm
KLEE: WARNING ONCE: function "k800_set_primary_pll_encoded" has inline asm
KLEE: WARNING ONCE: function "viafb_dvp0_proc_write" has inline asm
KLEE: WARNING ONCE: function "viafb_dvp0_proc_show" has inline asm
KLEE: WARNING ONCE: function "viafb_dvp1_proc_write" has inline asm
KLEE: WARNING ONCE: function "viafb_dvp1_proc_show" has inline asm
KLEE: WARNING ONCE: function "viafb_dfph_proc_write" has inline asm
KLEE: WARNING ONCE: function "viafb_dfph_proc_show" has inline asm
KLEE: WARNING ONCE: function "viafb_dfpl_proc_write" has inline asm
KLEE: WARNING ONCE: function "viafb_dfpl_proc_show" has inline asm
KLEE: WARNING ONCE: function "via_set_state" has inline asm
KLEE: WARNING ONCE: function "via_set_source" has inline asm
KLEE: WARNING ONCE: function "set_source_common" has inline asm
KLEE: WARNING ONCE: function "viafb_setmode" has inline asm
KLEE: WARNING ONCE: function "via_set_primary_address" has inline asm
KLEE: WARNING ONCE: function "via_set_secondary_address" has inline asm
KLEE: WARNING ONCE: function "viafb_dvi_disable" has inline asm
KLEE: WARNING ONCE: function "viafb_lcd_disable" has inline asm
KLEE: WARNING ONCE: function "viafb_write_regx" has inline asm
KLEE: WARNING ONCE: function "via_set_secondary_pitch" has inline asm
KLEE: WARNING ONCE: function "via_set_primary_color_depth" has inline asm
KLEE: WARNING ONCE: function "via_set_secondary_color_depth" has inline asm
KLEE: WARNING ONCE: function "viafb_lcd_set_mode" has inline asm
KLEE: WARNING ONCE: function "viafb_dvi_enable" has inline asm
KLEE: WARNING ONCE: function "viafb_lcd_enable" has inline asm
KLEE: WARNING ONCE: function "via_set_sync_polarity" has inline asm
KLEE: WARNING ONCE: function "set_lcd_output_path" has inline asm
KLEE: WARNING ONCE: function "integrated_lvds_enable" has inline asm
KLEE: WARNING ONCE: function "viafb_load_reg" has inline asm
KLEE: WARNING ONCE: function "via_set_primary_timing" has inline asm
KLEE: WARNING ONCE: function "via_set_secondary_timing" has inline asm
KLEE: WARNING ONCE: function "viafb_set_vclock" has inline asm
KLEE: WARNING ONCE: function "viafb_set_dpa_gfx" has inline asm
KLEE: WARNING ONCE: function "integrated_lvds_disable" has inline asm
KLEE: WARNING ONCE: function "viafb_wait_engine_idle" has inline asm
KLEE: WARNING ONCE: function "viafb_setcolreg" has inline asm
KLEE: WARNING ONCE: function "viafb_blank" has inline asm
KLEE: WARNING ONCE: function "viafb_cursor" has inline asm
KLEE: WARNING ONCE: function "viafb_ioctl" has inline asm
KLEE: WARNING ONCE: function "viafb_set_gamma_table" has inline asm
KLEE: WARNING ONCE: function "viafb_get_gamma_table" has inline asm
KLEE: WARNING ONCE: function "viafb_lcd_get_mobile_state" has inline asm
KLEE: WARNING ONCE: function "via_i2c_setsda" has inline asm
KLEE: WARNING ONCE: function "via_i2c_setscl" has inline asm
KLEE: WARNING ONCE: function "via_i2c_getsda" has inline asm
KLEE: WARNING ONCE: function "via_i2c_getscl" has inline asm
KLEE: WARNING ONCE: function "via_gpio_dir_input" has inline asm
KLEE: WARNING ONCE: function "via_gpio_get" has inline asm
KLEE: WARNING ONCE: function "via_gpio_set" has inline asm
KLEE: WARNING ONCE: function "viafb_gpio_probe" has inline asm
KLEE: WARNING ONCE: function "viafb_gpio_remove" has inline asm
KLEE: WARNING ONCE: function "viafb_gpio_resume" has inline asm
KLEE: WARNING ONCE: function "via_set_primary_pitch" has inline asm
KLEE: WARNING ONCE: function "viafb_unlock_crt" has inline asm
KLEE: WARNING ONCE: function "viafb_lock_crt" has inline asm
KLEE: WARNING ONCE: function "viafb_show_hw_cursor" has inline asm
KLEE: WARNING ONCE: function "viafb_set_primary_color_register" has inline asm
KLEE: WARNING ONCE: function "viafb_set_secondary_color_register" has inline asm
KLEE: WARNING ONCE: function "viafb_dma_copy_out_sg" has inline asm
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_9e83cb14-e508-4888-bca1-bcc766c1ceb6/symbiotic/lib/verifier/__VERIFIER_make_symbolic.c:8: wrong size given to klee_make_symbolic[_name]
KLEE: NOTE: now ignoring this error at this location
No error found.
RESULT: true
Generating witness: /tmp/vcloud-vcloud-master/worker/working_dir_9e83cb14-e508-4888-bca1-bcc766c1ceb6/symbiotic/witness.graphml
INFO: Total time elapsed: 2.28540086746
