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--isdn--hisax--hisax.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.: 2087 1527 17942 144087
Removed infinite loop in arch_local_save_flags
INFO: Compilation, preparation and instrumentation time: 4.51770687103
Removed calls to 'init_timer_key' (function is undefined)
Removed calls to 'add_timer' (function is undefined)
Defining function del_timer as symbolic
Removed calls to 'get_random_bytes' (function is undefined)
Defining function printk as symbolic
Defining function skb_put as symbolic
Defining function __alloc_skb as symbolic
Removed calls to 'skb_queue_purge' (function is undefined)
Removed calls to 'skb_queue_tail' (function is undefined)
Removed calls to 'consume_skb' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function skb_dequeue as symbolic
Defining function skb_realloc_headroom as symbolic
Defining function _raw_spin_lock_irqsave as symbolic
Defining function skb_clone as symbolic
Defining function skb_push as symbolic
Defining function skb_pull as symbolic
Defining function sprintf as symbolic
Defining function vsprintf as symbolic
Removed calls to 'skb_queue_head' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Defining function strcat as symbolic
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'msleep' (function is undefined)
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Defining function request_threaded_irq as symbolic
Removed calls to 'might_fault' (function is undefined)
Defining function register_isdn as symbolic
Defining function _copy_to_user as symbolic
Removed calls to '__release_region' (function is undefined)
Removed calls to 'iounmap' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Removed calls to 'pci_set_master' (function is undefined)
Removed calls to 'debug_dma_alloc_coherent' (function is undefined)
Removed calls to 'pci_dev_put' (function is undefined)
Defining function __request_region as symbolic
Removed calls to 'dev_kfree_skb_irq' (function is undefined)
Removed calls to 'dev_kfree_skb_any' (function is undefined)
Defining function schedule_work as symbolic
Defining function __netdev_alloc_skb as symbolic
Defining function __phys_addr as symbolic
Defining function pci_enable_device as symbolic
Defining function pci_dev_get as symbolic
Defining function pci_get_subsys as symbolic
Removed calls to '__wake_up' (function is undefined)
Defining function pci_bus_read_config_dword as symbolic
Defining function pci_bus_write_config_dword as symbolic
Defining function ioremap_nocache as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'debug_dma_free_coherent' (function is undefined)
Defining function pci_bus_write_config_word as symbolic
Defining function dma_supported as symbolic
Defining function dma_set_mask as symbolic
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Defining function _copy_from_user as symbolic
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'interruptible_sleep_on' (function is undefined)
Removed calls to 'ldv_handler_precall' (function is undefined)
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function mutex_trylock as symbolic
Linked our definitions to these undefined functions:
  strchr
  strcmp
  strcpy
  strlen
  strncpy
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 4.77057886124
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 2199 1233 12236 93986
INFO: Starting verification
KLEE: WARNING ONCE: function "l1_activate_no" has inline asm
KLEE: WARNING ONCE: function "l1_deact_req_s" has inline asm
KLEE: WARNING ONCE: function "l1_power_up_s" has inline asm
KLEE: WARNING ONCE: function "l1_info4_ind" has inline asm
KLEE: WARNING ONCE: function "l1_timer3" has inline asm
KLEE: WARNING ONCE: function "l1_timer_act" has inline asm
KLEE: WARNING ONCE: function "l1_timer_deact" has inline asm
KLEE: WARNING ONCE: function "L1deactivated" has inline asm
KLEE: WARNING ONCE: function "l1_deact_req_u" has inline asm
KLEE: WARNING ONCE: function "l1_power_up_u" has inline asm
KLEE: WARNING ONCE: function "l2_establish" has inline asm
KLEE: WARNING ONCE: function "l2_discard_i_setl3" has inline asm
KLEE: WARNING ONCE: function "l2_l3_reestablish" has inline asm
KLEE: WARNING ONCE: function "l2_pend_rel" has inline asm
KLEE: WARNING ONCE: function "l2_disconnect" has inline asm
KLEE: WARNING ONCE: function "l2_got_tei" has inline asm
KLEE: WARNING ONCE: function "l2_st5_tei_remove" has inline asm
KLEE: WARNING ONCE: function "l2_st6_tei_remove" has inline asm
KLEE: WARNING ONCE: function "l2_tei_remove" has inline asm
KLEE: WARNING ONCE: function "l2_start_multi" has inline asm
KLEE: WARNING ONCE: function "l2_restart_multi" has inline asm
KLEE: WARNING ONCE: function "l2_stop_multi" has inline asm
KLEE: WARNING ONCE: function "l2_connected" has inline asm
KLEE: WARNING ONCE: function "l2_released" has inline asm
KLEE: WARNING ONCE: function "l2_reestablish" has inline asm
KLEE: WARNING ONCE: function "l2_st5_dm_release" has inline asm
KLEE: WARNING ONCE: function "l2_st6_dm_release" has inline asm
KLEE: WARNING ONCE: function "l2_mdl_error_dm" has inline asm
KLEE: WARNING ONCE: function "l2_st8_mdl_error_dm" has inline asm
KLEE: WARNING ONCE: function "l2_got_FRMR" has inline asm
KLEE: WARNING ONCE: function "l2_st7_got_super" has inline asm
KLEE: WARNING ONCE: function "l2_st8_got_super" has inline asm
KLEE: WARNING ONCE: function "l2_got_iframe" has inline asm
KLEE: WARNING ONCE: function "l2_st5_tout_200" has inline asm
KLEE: WARNING ONCE: function "l2_st6_tout_200" has inline asm
KLEE: WARNING ONCE: function "l2_st7_tout_200" has inline asm
KLEE: WARNING ONCE: function "l2_st8_tout_200" has inline asm
KLEE: WARNING ONCE: function "l2_pull_iqueue" has inline asm
KLEE: WARNING ONCE: function "l2_set_own_busy" has inline asm
KLEE: WARNING ONCE: function "l2_clear_own_busy" has inline asm
KLEE: WARNING ONCE: function "l2_frame_error_reest" has inline asm
KLEE: WARNING ONCE: function "l2_st14_persistent_da" has inline asm
KLEE: WARNING ONCE: function "l2_st5_persistent_da" has inline asm
KLEE: WARNING ONCE: function "l2_st6_persistent_da" has inline asm
KLEE: WARNING ONCE: function "l2_persistent_da" has inline asm
KLEE: WARNING ONCE: function "establishlink" has inline asm
KLEE: WARNING ONCE: function "transmit_enquiry" has inline asm
KLEE: WARNING ONCE: function "enquiry_response" has inline asm
KLEE: WARNING ONCE: function "set_peer_busy" has inline asm
KLEE: WARNING ONCE: function "release_b_st" has inline asm
KLEE: WARNING ONCE: function "init_b_st" has inline asm
KLEE: WARNING ONCE: function "isdnl2_l1l2" has inline asm
KLEE: WARNING ONCE: function "isdnl2_l3l2" has inline asm
KLEE: WARNING ONCE: function "checkcard" has inline asm
KLEE: WARNING ONCE: function "HiSax_command" has inline asm
KLEE: WARNING ONCE: function "init_chan" has inline asm
KLEE: WARNING ONCE: function "dch_l2l1" has inline asm
KLEE: WARNING ONCE: function "BChannel_bh" has inline asm
KLEE: WARNING ONCE: function "setup_teles3" has inline asm
KLEE: WARNING ONCE: function "setup_telespci" has inline asm
KLEE: WARNING ONCE: function "setup_avm_a1_pcmcia" has inline asm
KLEE: WARNING ONCE: function "setup_avm_pcipnp" has inline asm
KLEE: WARNING ONCE: function "setup_elsa" has inline asm
KLEE: WARNING ONCE: function "setup_diva" has inline asm
KLEE: WARNING ONCE: function "setup_sedlbauer" has inline asm
KLEE: WARNING ONCE: function "setup_netjet_s" has inline asm
KLEE: WARNING ONCE: function "setup_hfcsx" has inline asm
KLEE: WARNING ONCE: function "setup_niccy" has inline asm
KLEE: WARNING ONCE: function "setup_sct_quadro" has inline asm
KLEE: WARNING ONCE: function "setup_gazel" has inline asm
KLEE: WARNING ONCE: function "setup_w6692" has inline asm
KLEE: WARNING ONCE: function "setup_netjet_u" has inline asm
KLEE: WARNING ONCE: function "setup_enternow_pci" has inline asm
KLEE: WARNING ONCE: function "ReadByteAmd7930" has inline asm
KLEE: WARNING ONCE: function "WriteByteAmd7930" has inline asm
KLEE: WARNING ONCE: function "enpci_setIrqMask" has inline asm
KLEE: WARNING ONCE: function "netjet_fill_dma" has inline asm
KLEE: WARNING ONCE: function "enpci_card_msg" has inline asm
KLEE: WARNING ONCE: function "enpci_interrupt" has inline asm
KLEE: WARNING ONCE: function "Amd7930_interrupt" has inline asm
KLEE: WARNING ONCE: function "write_raw" has inline asm
KLEE: WARNING ONCE: function "read_raw" has inline asm
KLEE: WARNING ONCE: function "Amd7930_fill_Dfifo" has inline asm
KLEE: WARNING ONCE: function "Amd7930_empty_Dfifo" has inline asm
KLEE: WARNING ONCE: function "reset_enpci" has inline asm
KLEE: WARNING ONCE: function "release_io_netjet" has inline asm
KLEE: WARNING ONCE: function "inittiger" has inline asm
KLEE: WARNING ONCE: function "setstack_tiger" has inline asm
KLEE: WARNING ONCE: function "close_tigerstate" has inline asm
KLEE: WARNING ONCE: function "mode_tiger" has inline asm
KLEE: WARNING ONCE: function "tiger_l2l1" has inline asm
KLEE: WARNING ONCE: function "Amd7930_l1hw" has inline asm
KLEE: WARNING ONCE: function "Amd7930_bh" has inline asm
KLEE: WARNING ONCE: function "dbusy_timer_handler___3" has inline asm
KLEE: WARNING ONCE: function "DChannel_proc_xmt" has inline asm
KLEE: WARNING ONCE: function "NETjet_ReadIC" has inline asm
KLEE: WARNING ONCE: function "NETjet_WriteIC" has inline asm
KLEE: WARNING ONCE: function "NETjet_ReadICfifo" has inline asm
KLEE: WARNING ONCE: function "NETjet_WriteICfifo" has inline asm
KLEE: WARNING ONCE: function "netjet_u_interrupt" has inline asm
KLEE: WARNING ONCE: function "icc_interrupt" has inline asm
KLEE: WARNING ONCE: function "icc_fill_fifo" has inline asm
KLEE: WARNING ONCE: function "reset_netjet_u" has inline asm
KLEE: WARNING ONCE: function "clear_pending_icc_ints" has inline asm
KLEE: WARNING ONCE: function "ICC_l1hw" has inline asm
KLEE: WARNING ONCE: function "icc_bh" has inline asm
KLEE: WARNING ONCE: function "dbusy_timer_handler___1" has inline asm
KLEE: WARNING ONCE: function "W6692_bh" has inline asm
KLEE: WARNING ONCE: function "ReadW6692" has inline asm
KLEE: WARNING ONCE: function "WriteW6692" has inline asm
KLEE: WARNING ONCE: function "ReadISACfifo___11" has inline asm
KLEE: WARNING ONCE: function "WriteISACfifo___11" has inline asm
KLEE: WARNING ONCE: function "ReadW6692B" has inline asm
KLEE: WARNING ONCE: function "WriteW6692B" has inline asm
KLEE: WARNING ONCE: function "W6692B_fill_fifo" has inline asm
KLEE: WARNING ONCE: function "W6692_interrupt" has inline asm
KLEE: WARNING ONCE: function "W6692_fill_fifo" has inline asm
KLEE: WARNING ONCE: function "W6692B_interrupt" has inline asm
KLEE: WARNING ONCE: function "W6692B_empty_fifo" has inline asm
KLEE: WARNING ONCE: function "dbusy_timer_handler___2" has inline asm
KLEE: WARNING ONCE: function "setstack_w6692" has inline asm
KLEE: WARNING ONCE: function "close_w6692state" has inline asm
KLEE: WARNING ONCE: function "W6692_l2l1" has inline asm
KLEE: WARNING ONCE: function "W6692_l1hw" has inline asm
KLEE: WARNING ONCE: function "reset_gazel" has inline asm
KLEE: WARNING ONCE: function "ReadISAC___10" has inline asm
KLEE: WARNING ONCE: function "WriteISAC___10" has inline asm
KLEE: WARNING ONCE: function "ReadISACfifo___10" has inline asm
KLEE: WARNING ONCE: function "WriteISACfifo___10" has inline asm
KLEE: WARNING ONCE: function "ReadHSCX___8" has inline asm
KLEE: WARNING ONCE: function "WriteHSCX___8" has inline asm
KLEE: WARNING ONCE: function "hscx_fill_fifo___8" has inline asm
KLEE: WARNING ONCE: function "isac_interrupt" has inline asm
KLEE: WARNING ONCE: function "isac_fill_fifo" has inline asm
KLEE: WARNING ONCE: function "hscx_interrupt___8" has inline asm
KLEE: WARNING ONCE: function "hscx_empty_fifo___8" has inline asm
KLEE: WARNING ONCE: function "clear_pending_isac_ints" has inline asm
KLEE: WARNING ONCE: function "close_hscxstate" has inline asm
KLEE: WARNING ONCE: function "open_hscxstate" has inline asm
KLEE: WARNING ONCE: function "hscx_l2l1" has inline asm
KLEE: WARNING ONCE: function "ISAC_l1hw" has inline asm
KLEE: WARNING ONCE: function "isac_bh" has inline asm
KLEE: WARNING ONCE: function "dbusy_timer_handler" has inline asm
KLEE: WARNING ONCE: function "arcofi_fsm" has inline asm
KLEE: WARNING ONCE: function "add_arcofi_timer" has inline asm
KLEE: WARNING ONCE: function "ReadISAC___9" has inline asm
KLEE: WARNING ONCE: function "WriteISAC___9" has inline asm
KLEE: WARNING ONCE: function "ReadISACfifo___9" has inline asm
KLEE: WARNING ONCE: function "WriteISACfifo___9" has inline asm
KLEE: WARNING ONCE: function "ReadHSCX___7" has inline asm
KLEE: WARNING ONCE: function "WriteHSCX___7" has inline asm
KLEE: WARNING ONCE: function "hscx_fill_fifo___7" has inline asm
KLEE: WARNING ONCE: function "BKM_card_msg___0" has inline asm
KLEE: WARNING ONCE: function "bkm_interrupt_ipac" has inline asm
KLEE: WARNING ONCE: function "WriteHSCXCMDR___7" has inline asm
KLEE: WARNING ONCE: function "hscx_interrupt___7" has inline asm
KLEE: WARNING ONCE: function "hscx_empty_fifo___7" has inline asm
KLEE: WARNING ONCE: function "jade_int_main" has inline asm
KLEE: WARNING ONCE: function "setstack_jade" has inline asm
KLEE: WARNING ONCE: function "close_jadestate" has inline asm
KLEE: WARNING ONCE: function "jade_l2l1" has inline asm
KLEE: WARNING ONCE: function "ReadISAC___7" has inline asm
KLEE: WARNING ONCE: function "WriteISAC___7" has inline asm
KLEE: WARNING ONCE: function "ReadISACfifo___7" has inline asm
KLEE: WARNING ONCE: function "WriteISACfifo___7" has inline asm
KLEE: WARNING ONCE: function "ReadHSCX___6" has inline asm
KLEE: WARNING ONCE: function "WriteHSCX___6" has inline asm
KLEE: WARNING ONCE: function "hscx_fill_fifo___6" has inline asm
KLEE: WARNING ONCE: function "niccy_interrupt" has inline asm
KLEE: WARNING ONCE: function "release_io_niccy" has inline asm
KLEE: WARNING ONCE: function "WriteHSCXCMDR___6" has inline asm
KLEE: WARNING ONCE: function "hscx_interrupt___6" has inline asm
KLEE: WARNING ONCE: function "hscx_empty_fifo___6" has inline asm
KLEE: WARNING ONCE: function "niccy_reset" has inline asm
KLEE: WARNING ONCE: function "hfcsx_bh" has inline asm
KLEE: WARNING ONCE: function "hfcsx_interrupt" has inline asm
KLEE: WARNING ONCE: function "reset_hfcsx" has inline asm
KLEE: WARNING ONCE: function "hfcsx_card_msg" has inline asm
KLEE: WARNING ONCE: function "hfcsx_auxcmd" has inline asm
KLEE: WARNING ONCE: function "hfcsx_send_data" has inline asm
KLEE: WARNING ONCE: function "setstack_2b___0" has inline asm
KLEE: WARNING ONCE: function "close_hfcsx" has inline asm
KLEE: WARNING ONCE: function "mode_hfcsx" has inline asm
KLEE: WARNING ONCE: function "reset_fifo" has inline asm
KLEE: WARNING ONCE: function "fifo_select" has inline asm
KLEE: WARNING ONCE: function "hfcsx_l2l1" has inline asm
KLEE: WARNING ONCE: function "hfcsx_fill_fifo" has inline asm
KLEE: WARNING ONCE: function "write_fifo___1" has inline asm
KLEE: WARNING ONCE: function "HFCSX_l1hw" has inline asm
KLEE: WARNING ONCE: function "main_rec_hfcsx" has inline asm
KLEE: WARNING ONCE: function "read_fifo___1" has inline asm
KLEE: WARNING ONCE: function "pci_free_consistent" has inline asm
KLEE: WARNING ONCE: function "hfcpci_bh" has inline asm
KLEE: WARNING ONCE: function "hfcpci_send_data" has inline asm
KLEE: WARNING ONCE: function "hfcpci_interrupt" has inline asm
KLEE: WARNING ONCE: function "setstack_2b" has inline asm
KLEE: WARNING ONCE: function "close_hfcpci" has inline asm
KLEE: WARNING ONCE: function "hfcpci_l2l1" has inline asm
KLEE: WARNING ONCE: function "main_rec_hfcpci" has inline asm
KLEE: WARNING ONCE: function "hfcpci_fill_fifo" has inline asm
KLEE: WARNING ONCE: function "HFCPCI_l1hw" has inline asm
KLEE: WARNING ONCE: function "netjet_s_interrupt" has inline asm
KLEE: WARNING ONCE: function "reset_netjet_s" has inline asm
KLEE: WARNING ONCE: function "ReadHSCX___5" has inline asm
KLEE: WARNING ONCE: function "WriteHSCX___5" has inline asm
KLEE: WARNING ONCE: function "hscx_fill_fifo___5" has inline asm
KLEE: WARNING ONCE: function "Sedl_card_msg" has inline asm
KLEE: WARNING ONCE: function "ReadISAC_IPAC___1" has inline asm
KLEE: WARNING ONCE: function "WriteISAC_IPAC___1" has inline asm
KLEE: WARNING ONCE: function "ReadISACfifo_IPAC___1" has inline asm
KLEE: WARNING ONCE: function "WriteISACfifo_IPAC___1" has inline asm
KLEE: WARNING ONCE: function "sedlbauer_interrupt_ipac" has inline asm
KLEE: WARNING ONCE: function "ReadISAC___6" has inline asm
KLEE: WARNING ONCE: function "WriteISAC___6" has inline asm
KLEE: WARNING ONCE: function "ReadISACfifo___6" has inline asm
KLEE: WARNING ONCE: function "WriteISACfifo___6" has inline asm
KLEE: WARNING ONCE: function "sedlbauer_interrupt_isar" has inline asm
KLEE: WARNING ONCE: function "isar_auxcmd" has inline asm
KLEE: WARNING ONCE: function "ReadISAR" has inline asm
KLEE: WARNING ONCE: function "WriteISAR" has inline asm
KLEE: WARNING ONCE: function "isar_fill_fifo" has inline asm
KLEE: WARNING ONCE: function "reset_sedlbauer" has inline asm
KLEE: WARNING ONCE: function "sedlbauer_interrupt" has inline asm
KLEE: WARNING ONCE: function "hscx_int_main___5" has inline asm
KLEE: WARNING ONCE: function "WriteHSCXCMDR___5" has inline asm
KLEE: WARNING ONCE: function "hscx_interrupt___5" has inline asm
KLEE: WARNING ONCE: function "hscx_empty_fifo___5" has inline asm
KLEE: WARNING ONCE: function "isar_pump_cmd" has inline asm
KLEE: WARNING ONCE: function "modeisar" has inline asm
KLEE: WARNING ONCE: function "isar_bh" has inline asm
KLEE: WARNING ONCE: function "isar_int_main" has inline asm
KLEE: WARNING ONCE: function "send_DLE_ETX" has inline asm
KLEE: WARNING ONCE: function "send_frames" has inline asm
KLEE: WARNING ONCE: function "setstack_isar" has inline asm
KLEE: WARNING ONCE: function "close_isarstate" has inline asm
KLEE: WARNING ONCE: function "ftimer_handler" has inline asm
KLEE: WARNING ONCE: function "isar_l2l1" has inline asm
KLEE: WARNING ONCE: function "ReadHSCX___4" has inline asm
KLEE: WARNING ONCE: function "WriteHSCX___4" has inline asm
KLEE: WARNING ONCE: function "hscx_fill_fifo___4" has inline asm
KLEE: WARNING ONCE: function "ReadISAC_IPAC___0" has inline asm
KLEE: WARNING ONCE: function "WriteISAC_IPAC___0" has inline asm
KLEE: WARNING ONCE: function "ReadISACfifo_IPAC___0" has inline asm
KLEE: WARNING ONCE: function "WriteISACfifo_IPAC___0" has inline asm
KLEE: WARNING ONCE: function "diva_irq_ipac_isa" has inline asm
KLEE: WARNING ONCE: function "diva_led_handler" has inline asm
KLEE: WARNING ONCE: function "ReadISAC___5" has inline asm
KLEE: WARNING ONCE: function "WriteISAC___5" has inline asm
KLEE: WARNING ONCE: function "ReadISACfifo___5" has inline asm
KLEE: WARNING ONCE: function "WriteISACfifo___5" has inline asm
KLEE: WARNING ONCE: function "diva_interrupt" has inline asm
KLEE: WARNING ONCE: function "release_io_diva" has inline asm
KLEE: WARNING ONCE: function "hscx_int_main___4" has inline asm
KLEE: WARNING ONCE: function "WriteHSCXCMDR___4" has inline asm
KLEE: WARNING ONCE: function "hscx_interrupt___4" has inline asm
KLEE: WARNING ONCE: function "hscx_empty_fifo___4" has inline asm
KLEE: WARNING ONCE: function "interrupt_ipacx" has inline asm
KLEE: WARNING ONCE: function "bch_int" has inline asm
KLEE: WARNING ONCE: function "dch_fill_fifo" has inline asm
KLEE: WARNING ONCE: function "Memhscx_interrupt" has inline asm
KLEE: WARNING ONCE: function "reset_diva" has inline asm
KLEE: WARNING ONCE: function "bch_setstack" has inline asm
KLEE: WARNING ONCE: function "bch_close_state" has inline asm
KLEE: WARNING ONCE: function "dbusy_timer_handler___0" has inline asm
KLEE: WARNING ONCE: function "dch_l2l1___0" has inline asm
KLEE: WARNING ONCE: function "bch_l2l1" has inline asm
KLEE: WARNING ONCE: function "probe_elsa_adr" has inline asm
KLEE: WARNING ONCE: function "init_arcofi" has inline asm
KLEE: WARNING ONCE: function "elsa_led_handler" has inline asm
KLEE: WARNING ONCE: function "TimerRun" has inline asm
KLEE: WARNING ONCE: function "release_io_elsa" has inline asm
KLEE: WARNING ONCE: function "ReadHSCX___3" has inline asm
KLEE: WARNING ONCE: function "WriteHSCX___3" has inline asm
KLEE: WARNING ONCE: function "hscx_fill_fifo___3" has inline asm
KLEE: WARNING ONCE: function "Elsa_card_msg" has inline asm
KLEE: WARNING ONCE: function "ReadISAC_IPAC" has inline asm
KLEE: WARNING ONCE: function "WriteISAC_IPAC" has inline asm
KLEE: WARNING ONCE: function "ReadISACfifo_IPAC" has inline asm
KLEE: WARNING ONCE: function "WriteISACfifo_IPAC" has inline asm
KLEE: WARNING ONCE: function "elsa_interrupt_ipac" has inline asm
KLEE: WARNING ONCE: function "ReadISAC___4" has inline asm
KLEE: WARNING ONCE: function "WriteISAC___4" has inline asm
KLEE: WARNING ONCE: function "ReadISACfifo___4" has inline asm
KLEE: WARNING ONCE: function "WriteISACfifo___4" has inline asm
KLEE: WARNING ONCE: function "elsa_interrupt" has inline asm
KLEE: WARNING ONCE: function "rs_interrupt_elsa" has inline asm
KLEE: WARNING ONCE: function "hscx_int_main___3" has inline asm
KLEE: WARNING ONCE: function "WriteHSCXCMDR___3" has inline asm
KLEE: WARNING ONCE: function "hscx_interrupt___3" has inline asm
KLEE: WARNING ONCE: function "hscx_empty_fifo___3" has inline asm
KLEE: WARNING ONCE: function "write_modem" has inline asm
KLEE: WARNING ONCE: function "reset_elsa" has inline asm
KLEE: WARNING ONCE: function "setstack_elsa" has inline asm
KLEE: WARNING ONCE: function "close_elsastate" has inline asm
KLEE: WARNING ONCE: function "mstartup" has inline asm
KLEE: WARNING ONCE: function "modem_write_cmd" has inline asm
KLEE: WARNING ONCE: function "modem_l2l1" has inline asm
KLEE: WARNING ONCE: function "ReadHDLC_s" has inline asm
KLEE: WARNING ONCE: function "WriteHDLC_s" has inline asm
KLEE: WARNING ONCE: function "ReadHDLCPnP" has inline asm
KLEE: WARNING ONCE: function "WriteHDLCPnP" has inline asm
KLEE: WARNING ONCE: function "ReadISAC___3" has inline asm
KLEE: WARNING ONCE: function "WriteISAC___3" has inline asm
KLEE: WARNING ONCE: function "ReadISACfifo___3" has inline asm
KLEE: WARNING ONCE: function "WriteISACfifo___3" has inline asm
KLEE: WARNING ONCE: function "hdlc_fill_fifo" has inline asm
KLEE: WARNING ONCE: function "AVM_card_msg___0" has inline asm
KLEE: WARNING ONCE: function "avm_pcipnp_interrupt" has inline asm
KLEE: WARNING ONCE: function "HDLC_irq" has inline asm
KLEE: WARNING ONCE: function "write_ctrl" has inline asm
KLEE: WARNING ONCE: function "reset_avmpcipnp" has inline asm
KLEE: WARNING ONCE: function "setstack_hdlc" has inline asm
KLEE: WARNING ONCE: function "close_hdlcstate" has inline asm
KLEE: WARNING ONCE: function "modehdlc" has inline asm
KLEE: WARNING ONCE: function "hdlc_l2l1" has inline asm
KLEE: WARNING ONCE: function "ReadISAC___2" has inline asm
KLEE: WARNING ONCE: function "WriteISAC___2" has inline asm
KLEE: WARNING ONCE: function "ReadISACfifo___2" has inline asm
KLEE: WARNING ONCE: function "WriteISACfifo___2" has inline asm
KLEE: WARNING ONCE: function "ReadHSCX___2" has inline asm
KLEE: WARNING ONCE: function "WriteHSCX___2" has inline asm
KLEE: WARNING ONCE: function "hscx_fill_fifo___2" has inline asm
KLEE: WARNING ONCE: function "AVM_card_msg" has inline asm
KLEE: WARNING ONCE: function "avm_a1p_interrupt" has inline asm
KLEE: WARNING ONCE: function "WriteHSCXCMDR___2" has inline asm
KLEE: WARNING ONCE: function "hscx_interrupt___2" has inline asm
KLEE: WARNING ONCE: function "hscx_empty_fifo___2" has inline asm
KLEE: WARNING ONCE: function "ReadISACfifo___0" has inline asm
KLEE: WARNING ONCE: function "WriteISACfifo___0" has inline asm
KLEE: WARNING ONCE: function "hscx_fill_fifo___0" has inline asm
KLEE: WARNING ONCE: function "telespci_interrupt" has inline asm
KLEE: WARNING ONCE: function "readisac" has inline asm
KLEE: WARNING ONCE: function "readhscx" has inline asm
KLEE: WARNING ONCE: function "hscx_interrupt___0" has inline asm
KLEE: WARNING ONCE: function "writehscx" has inline asm
KLEE: WARNING ONCE: function "writeisac" has inline asm
KLEE: WARNING ONCE: function "hscx_empty_fifo___0" has inline asm
KLEE: WARNING ONCE: function "readreg___0" has inline asm
KLEE: WARNING ONCE: function "hscx_interrupt___1" has inline asm
KLEE: WARNING ONCE: function "writereg___0" has inline asm
KLEE: WARNING ONCE: function "read_fifo___0" has inline asm
KLEE: WARNING ONCE: function "write_fifo___0" has inline asm
KLEE: WARNING ONCE: function "reset_teles3" has inline asm
KLEE: WARNING ONCE: function "ReadISAC" has inline asm
KLEE: WARNING ONCE: function "WriteISAC" has inline asm
KLEE: WARNING ONCE: function "ReadISACfifo" has inline asm
KLEE: WARNING ONCE: function "WriteISACfifo" has inline asm
KLEE: WARNING ONCE: function "ReadHSCX" has inline asm
KLEE: WARNING ONCE: function "WriteHSCX" has inline asm
KLEE: WARNING ONCE: function "hscx_fill_fifo" has inline asm
KLEE: WARNING ONCE: function "teles3_interrupt" has inline asm
KLEE: WARNING ONCE: function "WriteHSCXCMDR" has inline asm
KLEE: WARNING ONCE: function "hscx_interrupt" has inline asm
KLEE: WARNING ONCE: function "hscx_empty_fifo" has inline asm
KLEE: WARNING ONCE: function "clear_arcofi" has inline asm
KLEE: WARNING ONCE: function "hisax_register" has inline asm
KLEE: WARNING ONCE: function "hisax_bh" has inline asm
KLEE: WARNING ONCE: function "hisax_d_l2l1" has inline asm
KLEE: WARNING ONCE: function "hisax_b_l1l2" has inline asm
KLEE: WARNING ONCE: function "hisax_d_l1l2" has inline asm
KLEE: WARNING ONCE: function "hisax_b_l2l1" has inline asm
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: WARNING ONCE: flushing 9576 bytes on read, may be slow and/or crash: MO75[9576] allocated at global:
KLEE: ERROR: /tmp/symbiotic-tKVtKg/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--isdn--hisax--hisax.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:6640: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-tKVtKg/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--isdn--hisax--hisax.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:6640: invalid function pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: output directory is "/tmp/symbiotic-tKVtKg/klee-out-0"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: function "l1_activate_no" has inline asm
KLEE: WARNING ONCE: function "l1_deact_req_s" has inline asm
KLEE: WARNING ONCE: function "l1_power_up_s" has inline asm
KLEE: WARNING ONCE: function "l1_info4_ind" has inline asm
KLEE: WARNING ONCE: function "l1_timer3" has inline asm
KLEE: WARNING ONCE: function "l1_timer_act" has inline asm
KLEE: WARNING ONCE: function "l1_timer_deact" has inline asm
KLEE: WARNING ONCE: function "L1deactivated" has inline asm
KLEE: WARNING ONCE: function "l1_deact_req_u" has inline asm
KLEE: WARNING ONCE: function "l1_power_up_u" has inline asm
KLEE: WARNING ONCE: function "l2_establish" has inline asm
KLEE: WARNING ONCE: function "l2_discard_i_setl3" has inline asm
KLEE: WARNING ONCE: function "l2_l3_reestablish" has inline asm
KLEE: WARNING ONCE: function "l2_pend_rel" has inline asm
KLEE: WARNING ONCE: function "l2_disconnect" has inline asm
KLEE: WARNING ONCE: function "l2_got_tei" has inline asm
KLEE: WARNING ONCE: function "l2_st5_tei_remove" has inline asm
KLEE: WARNING ONCE: function "l2_st6_tei_remove" has inline asm
KLEE: WARNING ONCE: function "l2_tei_remove" has inline asm
KLEE: WARNING ONCE: function "l2_start_multi" has inline asm
KLEE: WARNING ONCE: function "l2_restart_multi" has inline asm
KLEE: WARNING ONCE: function "l2_stop_multi" has inline asm
KLEE: WARNING ONCE: function "l2_connected" has inline asm
KLEE: WARNING ONCE: function "l2_released" has inline asm
KLEE: WARNING ONCE: function "l2_reestablish" has inline asm
KLEE: WARNING ONCE: function "l2_st5_dm_release" has inline asm
KLEE: WARNING ONCE: function "l2_st6_dm_release" has inline asm
KLEE: WARNING ONCE: function "l2_mdl_error_dm" has inline asm
KLEE: WARNING ONCE: function "l2_st8_mdl_error_dm" has inline asm
KLEE: WARNING ONCE: function "l2_got_FRMR" has inline asm
KLEE: WARNING ONCE: function "l2_st7_got_super" has inline asm
KLEE: WARNING ONCE: function "l2_st8_got_super" has inline asm
KLEE: WARNING ONCE: function "l2_got_iframe" has inline asm
KLEE: WARNING ONCE: function "l2_st5_tout_200" has inline asm
KLEE: WARNING ONCE: function "l2_st6_tout_200" has inline asm
KLEE: WARNING ONCE: function "l2_st7_tout_200" has inline asm
KLEE: WARNING ONCE: function "l2_st8_tout_200" has inline asm
KLEE: WARNING ONCE: function "l2_pull_iqueue" has inline asm
KLEE: WARNING ONCE: function "l2_set_own_busy" has inline asm
KLEE: WARNING ONCE: function "l2_clear_own_busy" has inline asm
KLEE: WARNING ONCE: function "l2_frame_error_reest" has inline asm
KLEE: WARNING ONCE: function "l2_st14_persistent_da" has inline asm
KLEE: WARNING ONCE: function "l2_st5_persistent_da" has inline asm
KLEE: WARNING ONCE: function "l2_st6_persistent_da" has inline asm
KLEE: WARNING ONCE: function "l2_persistent_da" has inline asm
KLEE: WARNING ONCE: function "establishlink" has inline asm
KLEE: WARNING ONCE: function "transmit_enquiry" has inline asm
KLEE: WARNING ONCE: function "enquiry_response" has inline asm
KLEE: WARNING ONCE: function "set_peer_busy" has inline asm
KLEE: WARNING ONCE: function "release_b_st" has inline asm
KLEE: WARNING ONCE: function "init_b_st" has inline asm
KLEE: WARNING ONCE: function "isdnl2_l1l2" has inline asm
KLEE: WARNING ONCE: function "isdnl2_l3l2" has inline asm
KLEE: WARNING ONCE: function "checkcard" has inline asm
KLEE: WARNING ONCE: function "HiSax_command" has inline asm
KLEE: WARNING ONCE: function "init_chan" has inline asm
KLEE: WARNING ONCE: function "dch_l2l1" has inline asm
KLEE: WARNING ONCE: function "BChannel_bh" has inline asm
KLEE: WARNING ONCE: function "setup_teles3" has inline asm
KLEE: WARNING ONCE: function "setup_telespci" has inline asm
KLEE: WARNING ONCE: function "setup_avm_a1_pcmcia" has inline asm
KLEE: WARNING ONCE: function "setup_avm_pcipnp" has inline asm
KLEE: WARNING ONCE: function "setup_elsa" has inline asm
KLEE: WARNING ONCE: function "setup_diva" has inline asm
KLEE: WARNING ONCE: function "setup_sedlbauer" has inline asm
KLEE: WARNING ONCE: function "setup_netjet_s" has inline asm
KLEE: WARNING ONCE: function "setup_hfcsx" has inline asm
KLEE: WARNING ONCE: function "setup_niccy" has inline asm
KLEE: WARNING ONCE: function "setup_sct_quadro" has inline asm
KLEE: WARNING ONCE: function "setup_gazel" has inline asm
KLEE: WARNING ONCE: function "setup_w6692" has inline asm
KLEE: WARNING ONCE: function "setup_netjet_u" has inline asm
KLEE: WARNING ONCE: function "setup_enternow_pci" has inline asm
KLEE: WARNING ONCE: function "ReadByteAmd7930" has inline asm
KLEE: WARNING ONCE: function "WriteByteAmd7930" has inline asm
KLEE: WARNING ONCE: function "enpci_setIrqMask" has inline asm
KLEE: WARNING ONCE: function "netjet_fill_dma" has inline asm
KLEE: WARNING ONCE: function "enpci_card_msg" has inline asm
KLEE: WARNING ONCE: function "enpci_interrupt" has inline asm
KLEE: WARNING ONCE: function "Amd7930_interrupt" has inline asm
KLEE: WARNING ONCE: function "write_raw" has inline asm
KLEE: WARNING ONCE: function "read_raw" has inline asm
KLEE: WARNING ONCE: function "Amd7930_fill_Dfifo" has inline asm
KLEE: WARNING ONCE: function "Amd7930_empty_Dfifo" has inline asm
KLEE: WARNING ONCE: function "reset_enpci" has inline asm
KLEE: WARNING ONCE: function "release_io_netjet" has inline asm
KLEE: WARNING ONCE: function "inittiger" has inline asm
KLEE: WARNING ONCE: function "setstack_tiger" has inline asm
KLEE: WARNING ONCE: function "close_tigerstate" has inline asm
KLEE: WARNING ONCE: function "mode_tiger" has inline asm
KLEE: WARNING ONCE: function "tiger_l2l1" has inline asm
KLEE: WARNING ONCE: function "Amd7930_l1hw" has inline asm
KLEE: WARNING ONCE: function "Amd7930_bh" has inline asm
KLEE: WARNING ONCE: function "dbusy_timer_handler___3" has inline asm
KLEE: WARNING ONCE: function "DChannel_proc_xmt" has inline asm
KLEE: WARNING ONCE: function "NETjet_ReadIC" has inline asm
KLEE: WARNING ONCE: function "NETjet_WriteIC" has inline asm
KLEE: WARNING ONCE: function "NETjet_ReadICfifo" has inline asm
KLEE: WARNING ONCE: function "NETjet_WriteICfifo" has inline asm
KLEE: WARNING ONCE: function "netjet_u_interrupt" has inline asm
KLEE: WARNING ONCE: function "icc_interrupt" has inline asm
KLEE: WARNING ONCE: function "icc_fill_fifo" has inline asm
KLEE: WARNING ONCE: function "reset_netjet_u" has inline asm
KLEE: WARNING ONCE: function "clear_pending_icc_ints" has inline asm
KLEE: WARNING ONCE: function "ICC_l1hw" has inline asm
KLEE: WARNING ONCE: function "icc_bh" has inline asm
KLEE: WARNING ONCE: function "dbusy_timer_handler___1" has inline asm
KLEE: WARNING ONCE: function "W6692_bh" has inline asm
KLEE: WARNING ONCE: function "ReadW6692" has inline asm
KLEE: WARNING ONCE: function "WriteW6692" has inline asm
KLEE: WARNING ONCE: function "ReadISACfifo___11" has inline asm
KLEE: WARNING ONCE: function "WriteISACfifo___11" has inline asm
KLEE: WARNING ONCE: function "ReadW6692B" has inline asm
KLEE: WARNING ONCE: function "WriteW6692B" has inline asm
KLEE: WARNING ONCE: function "W6692B_fill_fifo" has inline asm
KLEE: WARNING ONCE: function "W6692_interrupt" has inline asm
KLEE: WARNING ONCE: function "W6692_fill_fifo" has inline asm
KLEE: WARNING ONCE: function "W6692B_interrupt" has inline asm
KLEE: WARNING ONCE: function "W6692B_empty_fifo" has inline asm
KLEE: WARNING ONCE: function "dbusy_timer_handler___2" has inline asm
KLEE: WARNING ONCE: function "setstack_w6692" has inline asm
KLEE: WARNING ONCE: function "close_w6692state" has inline asm
KLEE: WARNING ONCE: function "W6692_l2l1" has inline asm
KLEE: WARNING ONCE: function "W6692_l1hw" has inline asm
KLEE: WARNING ONCE: function "reset_gazel" has inline asm
KLEE: WARNING ONCE: function "ReadISAC___10" has inline asm
KLEE: WARNING ONCE: function "WriteISAC___10" has inline asm
KLEE: WARNING ONCE: function "ReadISACfifo___10" has inline asm
KLEE: WARNING ONCE: function "WriteISACfifo___10" has inline asm
KLEE: WARNING ONCE: function "ReadHSCX___8" has inline asm
KLEE: WARNING ONCE: function "WriteHSCX___8" has inline asm
KLEE: WARNING ONCE: function "hscx_fill_fifo___8" has inline asm
KLEE: WARNING ONCE: function "isac_interrupt" has inline asm
KLEE: WARNING ONCE: function "isac_fill_fifo" has inline asm
KLEE: WARNING ONCE: function "hscx_interrupt___8" has inline asm
KLEE: WARNING ONCE: function "hscx_empty_fifo___8" has inline asm
KLEE: WARNING ONCE: function "clear_pending_isac_ints" has inline asm
KLEE: WARNING ONCE: function "close_hscxstate" has inline asm
KLEE: WARNING ONCE: function "open_hscxstate" has inline asm
KLEE: WARNING ONCE: function "hscx_l2l1" has inline asm
KLEE: WARNING ONCE: function "ISAC_l1hw" has inline asm
KLEE: WARNING ONCE: function "isac_bh" has inline asm
KLEE: WARNING ONCE: function "dbusy_timer_handler" has inline asm
KLEE: WARNING ONCE: function "arcofi_fsm" has inline asm
KLEE: WARNING ONCE: function "add_arcofi_timer" has inline asm
KLEE: WARNING ONCE: function "ReadISAC___9" has inline asm
KLEE: WARNING ONCE: function "WriteISAC___9" has inline asm
KLEE: WARNING ONCE: function "ReadISACfifo___9" has inline asm
KLEE: WARNING ONCE: function "WriteISACfifo___9" has inline asm
KLEE: WARNING ONCE: function "ReadHSCX___7" has inline asm
KLEE: WARNING ONCE: function "WriteHSCX___7" has inline asm
KLEE: WARNING ONCE: function "hscx_fill_fifo___7" has inline asm
KLEE: WARNING ONCE: function "BKM_card_msg___0" has inline asm
KLEE: WARNING ONCE: function "bkm_interrupt_ipac" has inline asm
KLEE: WARNING ONCE: function "WriteHSCXCMDR___7" has inline asm
KLEE: WARNING ONCE: function "hscx_interrupt___7" has inline asm
KLEE: WARNING ONCE: function "hscx_empty_fifo___7" has inline asm
KLEE: WARNING ONCE: function "jade_int_main" has inline asm
KLEE: WARNING ONCE: function "setstack_jade" has inline asm
KLEE: WARNING ONCE: function "close_jadestate" has inline asm
KLEE: WARNING ONCE: function "jade_l2l1" has inline asm
KLEE: WARNING ONCE: function "ReadISAC___7" has inline asm
KLEE: WARNING ONCE: function "WriteISAC___7" has inline asm
KLEE: WARNING ONCE: function "ReadISACfifo___7" has inline asm
KLEE: WARNING ONCE: function "WriteISACfifo___7" has inline asm
KLEE: WARNING ONCE: function "ReadHSCX___6" has inline asm
KLEE: WARNING ONCE: function "WriteHSCX___6" has inline asm
KLEE: WARNING ONCE: function "hscx_fill_fifo___6" has inline asm
KLEE: WARNING ONCE: function "niccy_interrupt" has inline asm
KLEE: WARNING ONCE: function "release_io_niccy" has inline asm
KLEE: WARNING ONCE: function "WriteHSCXCMDR___6" has inline asm
KLEE: WARNING ONCE: function "hscx_interrupt___6" has inline asm
KLEE: WARNING ONCE: function "hscx_empty_fifo___6" has inline asm
KLEE: WARNING ONCE: function "niccy_reset" has inline asm
KLEE: WARNING ONCE: function "hfcsx_bh" has inline asm
KLEE: WARNING ONCE: function "hfcsx_interrupt" has inline asm
KLEE: WARNING ONCE: function "reset_hfcsx" has inline asm
KLEE: WARNING ONCE: function "hfcsx_card_msg" has inline asm
KLEE: WARNING ONCE: function "hfcsx_auxcmd" has inline asm
KLEE: WARNING ONCE: function "hfcsx_send_data" has inline asm
KLEE: WARNING ONCE: function "setstack_2b___0" has inline asm
KLEE: WARNING ONCE: function "close_hfcsx" has inline asm
KLEE: WARNING ONCE: function "mode_hfcsx" has inline asm
KLEE: WARNING ONCE: function "reset_fifo" has inline asm
KLEE: WARNING ONCE: function "fifo_select" has inline asm
KLEE: WARNING ONCE: function "hfcsx_l2l1" has inline asm
KLEE: WARNING ONCE: function "hfcsx_fill_fifo" has inline asm
KLEE: WARNING ONCE: function "write_fifo___1" has inline asm
KLEE: WARNING ONCE: function "HFCSX_l1hw" has inline asm
KLEE: WARNING ONCE: function "main_rec_hfcsx" has inline asm
KLEE: WARNING ONCE: function "read_fifo___1" has inline asm
KLEE: WARNING ONCE: function "pci_free_consistent" has inline asm
KLEE: WARNING ONCE: function "hfcpci_bh" has inline asm
KLEE: WARNING ONCE: function "hfcpci_send_data" has inline asm
KLEE: WARNING ONCE: function "hfcpci_interrupt" has inline asm
KLEE: WARNING ONCE: function "setstack_2b" has inline asm
KLEE: WARNING ONCE: function "close_hfcpci" has inline asm
KLEE: WARNING ONCE: function "hfcpci_l2l1" has inline asm
KLEE: WARNING ONCE: function "main_rec_hfcpci" has inline asm
KLEE: WARNING ONCE: function "hfcpci_fill_fifo" has inline asm
KLEE: WARNING ONCE: function "HFCPCI_l1hw" has inline asm
KLEE: WARNING ONCE: function "netjet_s_interrupt" has inline asm
KLEE: WARNING ONCE: function "reset_netjet_s" has inline asm
KLEE: WARNING ONCE: function "ReadHSCX___5" has inline asm
KLEE: WARNING ONCE: function "WriteHSCX___5" has inline asm
KLEE: WARNING ONCE: function "hscx_fill_fifo___5" has inline asm
KLEE: WARNING ONCE: function "Sedl_card_msg" has inline asm
KLEE: WARNING ONCE: function "ReadISAC_IPAC___1" has inline asm
KLEE: WARNING ONCE: function "WriteISAC_IPAC___1" has inline asm
KLEE: WARNING ONCE: function "ReadISACfifo_IPAC___1" has inline asm
KLEE: WARNING ONCE: function "WriteISACfifo_IPAC___1" has inline asm
KLEE: WARNING ONCE: function "sedlbauer_interrupt_ipac" has inline asm
KLEE: WARNING ONCE: function "ReadISAC___6" has inline asm
KLEE: WARNING ONCE: function "WriteISAC___6" has inline asm
KLEE: WARNING ONCE: function "ReadISACfifo___6" has inline asm
KLEE: WARNING ONCE: function "WriteISACfifo___6" has inline asm
KLEE: WARNING ONCE: function "sedlbauer_interrupt_isar" has inline asm
KLEE: WARNING ONCE: function "isar_auxcmd" has inline asm
KLEE: WARNING ONCE: function "ReadISAR" has inline asm
KLEE: WARNING ONCE: function "WriteISAR" has inline asm
KLEE: WARNING ONCE: function "isar_fill_fifo" has inline asm
KLEE: WARNING ONCE: function "reset_sedlbauer" has inline asm
KLEE: WARNING ONCE: function "sedlbauer_interrupt" has inline asm
KLEE: WARNING ONCE: function "hscx_int_main___5" has inline asm
KLEE: WARNING ONCE: function "WriteHSCXCMDR___5" has inline asm
KLEE: WARNING ONCE: function "hscx_interrupt___5" has inline asm
KLEE: WARNING ONCE: function "hscx_empty_fifo___5" has inline asm
KLEE: WARNING ONCE: function "isar_pump_cmd" has inline asm
KLEE: WARNING ONCE: function "modeisar" has inline asm
KLEE: WARNING ONCE: function "isar_bh" has inline asm
KLEE: WARNING ONCE: function "isar_int_main" has inline asm
KLEE: WARNING ONCE: function "send_DLE_ETX" has inline asm
KLEE: WARNING ONCE: function "send_frames" has inline asm
KLEE: WARNING ONCE: function "setstack_isar" has inline asm
KLEE: WARNING ONCE: function "close_isarstate" has inline asm
KLEE: WARNING ONCE: function "ftimer_handler" has inline asm
KLEE: WARNING ONCE: function "isar_l2l1" has inline asm
KLEE: WARNING ONCE: function "ReadHSCX___4" has inline asm
KLEE: WARNING ONCE: function "WriteHSCX___4" has inline asm
KLEE: WARNING ONCE: function "hscx_fill_fifo___4" has inline asm
KLEE: WARNING ONCE: function "ReadISAC_IPAC___0" has inline asm
KLEE: WARNING ONCE: function "WriteISAC_IPAC___0" has inline asm
KLEE: WARNING ONCE: function "ReadISACfifo_IPAC___0" has inline asm
KLEE: WARNING ONCE: function "WriteISACfifo_IPAC___0" has inline asm
KLEE: WARNING ONCE: function "diva_irq_ipac_isa" has inline asm
KLEE: WARNING ONCE: function "diva_led_handler" has inline asm
KLEE: WARNING ONCE: function "ReadISAC___5" has inline asm
KLEE: WARNING ONCE: function "WriteISAC___5" has inline asm
KLEE: WARNING ONCE: function "ReadISACfifo___5" has inline asm
KLEE: WARNING ONCE: function "WriteISACfifo___5" has inline asm
KLEE: WARNING ONCE: function "diva_interrupt" has inline asm
KLEE: WARNING ONCE: function "release_io_diva" has inline asm
KLEE: WARNING ONCE: function "hscx_int_main___4" has inline asm
KLEE: WARNING ONCE: function "WriteHSCXCMDR___4" has inline asm
KLEE: WARNING ONCE: function "hscx_interrupt___4" has inline asm
KLEE: WARNING ONCE: function "hscx_empty_fifo___4" has inline asm
KLEE: WARNING ONCE: function "interrupt_ipacx" has inline asm
KLEE: WARNING ONCE: function "bch_int" has inline asm
KLEE: WARNING ONCE: function "dch_fill_fifo" has inline asm
KLEE: WARNING ONCE: function "Memhscx_interrupt" has inline asm
KLEE: WARNING ONCE: function "reset_diva" has inline asm
KLEE: WARNING ONCE: function "bch_setstack" has inline asm
KLEE: WARNING ONCE: function "bch_close_state" has inline asm
KLEE: WARNING ONCE: function "dbusy_timer_handler___0" has inline asm
KLEE: WARNING ONCE: function "dch_l2l1___0" has inline asm
KLEE: WARNING ONCE: function "bch_l2l1" has inline asm
KLEE: WARNING ONCE: function "probe_elsa_adr" has inline asm
KLEE: WARNING ONCE: function "init_arcofi" has inline asm
KLEE: WARNING ONCE: function "elsa_led_handler" has inline asm
KLEE: WARNING ONCE: function "TimerRun" has inline asm
KLEE: WARNING ONCE: function "release_io_elsa" has inline asm
KLEE: WARNING ONCE: function "ReadHSCX___3" has inline asm
KLEE: WARNING ONCE: function "WriteHSCX___3" has inline asm
KLEE: WARNING ONCE: function "hscx_fill_fifo___3" has inline asm
KLEE: WARNING ONCE: function "Elsa_card_msg" has inline asm
KLEE: WARNING ONCE: function "ReadISAC_IPAC" has inline asm
KLEE: WARNING ONCE: function "WriteISAC_IPAC" has inline asm
KLEE: WARNING ONCE: function "ReadISACfifo_IPAC" has inline asm
KLEE: WARNING ONCE: function "WriteISACfifo_IPAC" has inline asm
KLEE: WARNING ONCE: function "elsa_interrupt_ipac" has inline asm
KLEE: WARNING ONCE: function "ReadISAC___4" has inline asm
KLEE: WARNING ONCE: function "WriteISAC___4" has inline asm
KLEE: WARNING ONCE: function "ReadISACfifo___4" has inline asm
KLEE: WARNING ONCE: function "WriteISACfifo___4" has inline asm
KLEE: WARNING ONCE: function "elsa_interrupt" has inline asm
KLEE: WARNING ONCE: function "rs_interrupt_elsa" has inline asm
KLEE: WARNING ONCE: function "hscx_int_main___3" has inline asm
KLEE: WARNING ONCE: function "WriteHSCXCMDR___3" has inline asm
KLEE: WARNING ONCE: function "hscx_interrupt___3" has inline asm
KLEE: WARNING ONCE: function "hscx_empty_fifo___3" has inline asm
KLEE: WARNING ONCE: function "write_modem" has inline asm
KLEE: WARNING ONCE: function "reset_elsa" has inline asm
KLEE: WARNING ONCE: function "setstack_elsa" has inline asm
KLEE: WARNING ONCE: function "close_elsastate" has inline asm
KLEE: WARNING ONCE: function "mstartup" has inline asm
KLEE: WARNING ONCE: function "modem_write_cmd" has inline asm
KLEE: WARNING ONCE: function "modem_l2l1" has inline asm
KLEE: WARNING ONCE: function "ReadHDLC_s" has inline asm
KLEE: WARNING ONCE: function "WriteHDLC_s" has inline asm
KLEE: WARNING ONCE: function "ReadHDLCPnP" has inline asm
KLEE: WARNING ONCE: function "WriteHDLCPnP" has inline asm
KLEE: WARNING ONCE: function "ReadISAC___3" has inline asm
KLEE: WARNING ONCE: function "WriteISAC___3" has inline asm
KLEE: WARNING ONCE: function "ReadISACfifo___3" has inline asm
KLEE: WARNING ONCE: function "WriteISACfifo___3" has inline asm
KLEE: WARNING ONCE: function "hdlc_fill_fifo" has inline asm
KLEE: WARNING ONCE: function "AVM_card_msg___0" has inline asm
KLEE: WARNING ONCE: function "avm_pcipnp_interrupt" has inline asm
KLEE: WARNING ONCE: function "HDLC_irq" has inline asm
KLEE: WARNING ONCE: function "write_ctrl" has inline asm
KLEE: WARNING ONCE: function "reset_avmpcipnp" has inline asm
KLEE: WARNING ONCE: function "setstack_hdlc" has inline asm
KLEE: WARNING ONCE: function "close_hdlcstate" has inline asm
KLEE: WARNING ONCE: function "modehdlc" has inline asm
KLEE: WARNING ONCE: function "hdlc_l2l1" has inline asm
KLEE: WARNING ONCE: function "ReadISAC___2" has inline asm
KLEE: WARNING ONCE: function "WriteISAC___2" has inline asm
KLEE: WARNING ONCE: function "ReadISACfifo___2" has inline asm
KLEE: WARNING ONCE: function "WriteISACfifo___2" has inline asm
KLEE: WARNING ONCE: function "ReadHSCX___2" has inline asm
KLEE: WARNING ONCE: function "WriteHSCX___2" has inline asm
KLEE: WARNING ONCE: function "hscx_fill_fifo___2" has inline asm
KLEE: WARNING ONCE: function "AVM_card_msg" has inline asm
KLEE: WARNING ONCE: function "avm_a1p_interrupt" has inline asm
KLEE: WARNING ONCE: function "WriteHSCXCMDR___2" has inline asm
KLEE: WARNING ONCE: function "hscx_interrupt___2" has inline asm
KLEE: WARNING ONCE: function "hscx_empty_fifo___2" has inline asm
KLEE: WARNING ONCE: function "ReadISACfifo___0" has inline asm
KLEE: WARNING ONCE: function "WriteISACfifo___0" has inline asm
KLEE: WARNING ONCE: function "hscx_fill_fifo___0" has inline asm
KLEE: WARNING ONCE: function "telespci_interrupt" has inline asm
KLEE: WARNING ONCE: function "readisac" has inline asm
KLEE: WARNING ONCE: function "readhscx" has inline asm
KLEE: WARNING ONCE: function "hscx_interrupt___0" has inline asm
KLEE: WARNING ONCE: function "writehscx" has inline asm
KLEE: WARNING ONCE: function "writeisac" has inline asm
KLEE: WARNING ONCE: function "hscx_empty_fifo___0" has inline asm
KLEE: WARNING ONCE: function "readreg___0" has inline asm
KLEE: WARNING ONCE: function "hscx_interrupt___1" has inline asm
KLEE: WARNING ONCE: function "writereg___0" has inline asm
KLEE: WARNING ONCE: function "read_fifo___0" has inline asm
KLEE: WARNING ONCE: function "write_fifo___0" has inline asm
KLEE: WARNING ONCE: function "reset_teles3" has inline asm
KLEE: WARNING ONCE: function "ReadISAC" has inline asm
KLEE: WARNING ONCE: function "WriteISAC" has inline asm
KLEE: WARNING ONCE: function "ReadISACfifo" has inline asm
KLEE: WARNING ONCE: function "WriteISACfifo" has inline asm
KLEE: WARNING ONCE: function "ReadHSCX" has inline asm
KLEE: WARNING ONCE: function "WriteHSCX" has inline asm
KLEE: WARNING ONCE: function "hscx_fill_fifo" has inline asm
KLEE: WARNING ONCE: function "teles3_interrupt" has inline asm
KLEE: WARNING ONCE: function "WriteHSCXCMDR" has inline asm
KLEE: WARNING ONCE: function "hscx_interrupt" has inline asm
KLEE: WARNING ONCE: function "hscx_empty_fifo" has inline asm
KLEE: WARNING ONCE: function "clear_arcofi" has inline asm
KLEE: WARNING ONCE: function "hisax_register" has inline asm
KLEE: WARNING ONCE: function "hisax_bh" has inline asm
KLEE: WARNING ONCE: function "hisax_d_l2l1" has inline asm
KLEE: WARNING ONCE: function "hisax_b_l1l2" has inline asm
KLEE: WARNING ONCE: function "hisax_d_l1l2" has inline asm
KLEE: WARNING ONCE: function "hisax_b_l2l1" has inline asm
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: WARNING ONCE: flushing 9576 bytes on read, may be slow and/or crash: MO75[9576] allocated at global:
KLEE: ERROR: /tmp/symbiotic-tKVtKg/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--isdn--hisax--hisax.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:6640: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-tKVtKg/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--isdn--hisax--hisax.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:6640: invalid function pointer
KLEE: NOTE: now ignoring this error at this location
0  klee            0x00000000012fcca8 llvm::sys::PrintStackTrace(llvm::raw_ostream&) + 56
1  klee            0x00000000012fac7e llvm::sys::RunSignalHandlers() + 62
2  klee            0x00000000012fadcc
3  libpthread.so.0 0x00007f630adfb390
4  klee            0x0000000000a59836 klee::EqExpr::create(klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&) + 38
5  klee            0x00000000005d7c3c klee::Executor::executeInstruction(klee::ExecutionState&, klee::KInstruction*) + 12060
6  klee            0x00000000005da8c5 klee::Executor::run(klee::ExecutionState&) + 2117
7  klee            0x00000000005daeef klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1391
8  klee            0x0000000000593c63 main + 8867
9  libc.so.6       0x00007f630a19f830 __libc_start_main + 240
10 klee            0x00000000005bed49 _start + 41
Running the verifier failed
RESULT: unknown
INFO: Total time elapsed: 342.692719936
