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_false-unreach-call_linux-3.8-rc1-32_7a-fs--ubifs--ubifs.ko-ldv_main3_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.: 1409 1275 16262 124144
Removed infinite loop in get_dent_type
Removed infinite loop in ubifs_tnc_has_node
Removed infinite loop in ubifs_new_inode
Removed infinite loop in vfs_dent_type
INFO: Compilation, preparation and instrumentation time: 3.59525609016
Removed calls to 'dump_stack' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'unlock_page' (function is undefined)
Removed calls to 'put_page' (function is undefined)
Removed calls to '__mark_inode_dirty' (function is undefined)
Defining function printk as symbolic
Removed calls to 'truncate_setsize' (function is undefined)
Removed calls to 'generic_fillattr' (function is undefined)
Removed calls to '__insert_inode_hash' (function is undefined)
Removed calls to 'iput' (function is undefined)
Removed calls to 'make_bad_inode' (function is undefined)
Removed calls to 'clear_nlink' (function is undefined)
Removed calls to 'set_nlink' (function is undefined)
Removed calls to 'down_read' (function is undefined)
Removed calls to 'writeback_inodes_sb' (function is undefined)
Removed calls to 'up_read' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'down_write' (function is undefined)
Removed calls to 'up_write' (function is undefined)
Removed calls to 'print_hex_dump' (function is undefined)
Defining function strnlen as symbolic
Defining function ubi_is_mapped as symbolic
Defining function crc32_le as symbolic
Defining function ubi_leb_read as symbolic
Removed calls to 'rb_insert_color' (function is undefined)
Defining function get_seconds as symbolic
Defining function snprintf as symbolic
Removed calls to 'list_del' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Defining function crc16 as symbolic
Defining function ubi_leb_write as symbolic
Removed calls to 'prandom_bytes' (function is undefined)
Defining function prandom_u32 as symbolic
Defining function msecs_to_jiffies as symbolic
Defining function hrtimer_cancel as symbolic
Removed calls to 'vfree' (function is undefined)
Defining function __vmalloc as symbolic
Defining function _cond_resched as symbolic
Defining function hrtimer_start_range_ns as symbolic
Defining function kmemdup as symbolic
Removed calls to 'mutex_lock_nested' (function is undefined)
Defining function rb_first as symbolic
Defining function rb_next as symbolic
Removed calls to 'prepare_to_wait' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Removed calls to 'rb_erase' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Defining function ubi_leb_unmap as symbolic
Defining function ubi_leb_change as symbolic
Removed calls to 'sort' (function is undefined)
Defining function autoremove_wake_function as symbolic
Defining function ubi_leb_map as symbolic
Defining function wake_up_process as symbolic
Defining function down_write_trylock as symbolic
Removed calls to 'list_sort' (function is undefined)
Defining function current_fs_time as symbolic
Defining function debug_lockdep_rcu_enabled as symbolic
Defining function capable as symbolic
Defining function in_group_p as symbolic
Removed calls to 'init_special_inode' (function is undefined)
Removed calls to 'unlock_new_inode' (function is undefined)
Removed calls to 'iget_failed' (function is undefined)
Defining function iget_locked as symbolic
Removed calls to 'inode_init_owner' (function is undefined)
Defining function new_inode as symbolic
Defining function inode_change_ok as symbolic
Defining function timespec_trunc as symbolic
Defining function find_lock_page as symbolic
Defining function clear_page_dirty_for_io as symbolic
Removed calls to 'end_page_writeback' (function is undefined)
Defining function test_set_page_writeback as symbolic
Defining function generic_readlink as symbolic
Defining function generic_file_llseek as symbolic
Defining function do_sync_read as symbolic
Defining function do_sync_write as symbolic
Defining function generic_file_aio_read as symbolic
Removed calls to 'might_fault' (function is undefined)
Removed calls to 'mnt_drop_write_file' (function is undefined)
Defining function generic_file_splice_write as symbolic
Defining function generic_file_splice_read as symbolic
Defining function filemap_write_and_wait_range as symbolic
Defining function generic_file_mmap as symbolic
Defining function inode_owner_or_capable as symbolic
Defining function mnt_want_write_file as symbolic
Defining function write_inode_now as symbolic
Defining function generic_file_aio_write as symbolic
Removed calls to 'd_instantiate' (function is undefined)
Removed calls to 'd_rehash' (function is undefined)
Removed calls to 'inc_nlink' (function is undefined)
Removed calls to 'ihold' (function is undefined)
Removed calls to 'drop_nlink' (function is undefined)
Defining function generic_read_dir as symbolic
Removed calls to '__mutex_init' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'call_rcu_sched' (function is undefined)
Removed calls to 'truncate_inode_pages' (function is undefined)
Removed calls to 'clear_inode' (function is undefined)
Removed calls to 'bdi_destroy' (function is undefined)
Removed calls to 'ubi_close_volume' (function is undefined)
Defining function seq_printf as symbolic
Defining function kthread_stop as symbolic
Defining function vmalloc as symbolic
Defining function kthread_create_on_node as symbolic
Defining function set_freezable as symbolic
Defining function kthread_should_stop as symbolic
Defining function __refrigerator as symbolic
Defining function freezing_slow_path as symbolic
Defining function match_token as symbolic
Defining function match_strdup as symbolic
Defining function strsep as symbolic
Defining function ubi_sync as symbolic
Removed calls to 'debugfs_remove_recursive' (function is undefined)
Defining function is_bad_inode as symbolic
Removed calls to 'kmem_cache_free' (function is undefined)
Defining function kmem_cache_alloc as symbolic
Defining function filemap_fault as symbolic
Removed calls to '__lock_page' (function is undefined)
Defining function generic_file_remap_pages as symbolic
Defining function __set_page_dirty_nobuffers as symbolic
Defining function mutex_trylock as symbolic
Removed calls to '__init_rwsem' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'ubi_get_volume_info' (function is undefined)
Removed calls to 'deactivate_locked_super' (function is undefined)
Removed calls to 'kill_anon_super' (function is undefined)
Defining function sget as symbolic
Defining function ubi_open_volume as symbolic
Defining function bdi_init as symbolic
Defining function bdi_register as symbolic
Defining function d_make_root as symbolic
Removed calls to 'generate_random_uuid' (function is undefined)
Defining function sprintf as symbolic
Defining function debugfs_create_dir as symbolic
Defining function debugfs_create_file as symbolic
Defining function ilookup as symbolic
Removed calls to 'hrtimer_init' (function is undefined)
Defining function set_anon_super as symbolic
Defining function ubi_get_device_info as symbolic
Defining function ubi_open_volume_path as symbolic
Defining function ubi_open_volume_nm as symbolic
Defining function no_llseek as symbolic
Defining function nonseekable_open as symbolic
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Defining function _copy_from_user as symbolic
Defining function simple_read_from_buffer as symbolic
Defining function grab_cache_page_write_begin as symbolic
Defining function find_or_create_page as symbolic
Removed calls to 'ldv_handler_precall' (function is undefined)
Removed calls to 'unregister_shrinker' (function is undefined)
Removed calls to 'rcu_barrier' (function is undefined)
Removed calls to 'kmem_cache_destroy' (function is undefined)
Defining function unregister_filesystem as symbolic
Defining function crypto_alloc_base as symbolic
Removed calls to 'ldv_check_return_value' (function is undefined)
Linked our definitions to these undefined functions:
  memcmp
  strcmp
  strlen
  strncmp
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 3.87125587463
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 1591 987 9264 65996
INFO: Starting verification
KLEE: WARNING ONCE: function "ubifs_writepage" has inline asm
KLEE: WARNING ONCE: function "ubifs_readpage" has inline asm
KLEE: WARNING ONCE: function "ubifs_set_page_dirty" has inline asm
KLEE: WARNING ONCE: function "ubifs_write_begin" has inline asm
KLEE: WARNING ONCE: function "ubifs_write_end" has inline asm
KLEE: WARNING ONCE: function "ubifs_invalidatepage" has inline asm
KLEE: WARNING ONCE: function "ubifs_releasepage" has inline asm
KLEE: WARNING ONCE: function "ubifs_setattr" has inline asm
KLEE: WARNING ONCE: function "ubifs_setxattr" has inline asm
KLEE: WARNING ONCE: function "ubifs_getxattr" has inline asm
KLEE: WARNING ONCE: function "ubifs_listxattr" has inline asm
KLEE: WARNING ONCE: function "ubifs_removexattr" has inline asm
KLEE: WARNING ONCE: function "xent_key_init" has inline asm
KLEE: WARNING ONCE: function "ubifs_tnc_lookup_nm" has inline asm
KLEE: WARNING ONCE: function "iget_xattr" has inline asm
KLEE: WARNING ONCE: function "ubifs_budget_space" has inline asm
KLEE: WARNING ONCE: function "ubifs_jnl_delete_xattr" has inline asm
KLEE: WARNING ONCE: function "ubifs_release_budget" has inline asm
KLEE: WARNING ONCE: function "make_reservation" has inline asm
KLEE: WARNING ONCE: function "get_dent_type" has inline asm
KLEE: WARNING ONCE: function "ubifs_prep_grp_node" has inline asm
KLEE: WARNING ONCE: function "ubifs_update_one_lp" has inline asm
KLEE: WARNING ONCE: function "ubifs_ro_mode" has inline asm
KLEE: WARNING ONCE: function "tnc_insert" has inline asm
KLEE: WARNING ONCE: function "dbg_check_tnc" has inline asm
KLEE: WARNING ONCE: function "ubifs_search_zbranch" has inline asm
KLEE: WARNING ONCE: function "dbg_check_key_order" has inline asm
KLEE: WARNING ONCE: function "ubifs_tnc_postorder_next" has inline asm
KLEE: WARNING ONCE: function "dbg_snprintf_key" has inline asm
KLEE: WARNING ONCE: function "ubifs_tnc_read_node" has inline asm
KLEE: WARNING ONCE: function "ubifs_validate_entry" has inline asm
KLEE: WARNING ONCE: function "ubifs_read_node_wbuf" has inline asm
KLEE: WARNING ONCE: function "ubifs_read_node" has inline asm
KLEE: WARNING ONCE: function "ubifs_leb_read" has inline asm
KLEE: WARNING ONCE: function "ubifs_check_node" has inline asm
KLEE: WARNING ONCE: function "insert_zbranch" has inline asm
KLEE: WARNING ONCE: function "correct_parent_keys" has inline asm
KLEE: WARNING ONCE: function "insert_old_idx" has inline asm
KLEE: WARNING ONCE: function "ubifs_load_znode" has inline asm
KLEE: WARNING ONCE: function "dirty_cow_znode" has inline asm
KLEE: WARNING ONCE: function "dirty_cow_bottom_up" has inline asm
KLEE: WARNING ONCE: function "ubifs_lookup_level0" has inline asm
KLEE: WARNING ONCE: function "tnc_delete" has inline asm
KLEE: WARNING ONCE: function "ubifs_lpt_lookup_dirty" has inline asm
KLEE: WARNING ONCE: function "ubifs_change_lp" has inline asm
KLEE: WARNING ONCE: function "ubifs_release_lprops___3" has inline asm
KLEE: WARNING ONCE: function "ubifs_calc_dark" has inline asm
KLEE: WARNING ONCE: function "ubifs_categorize_lprops" has inline asm
KLEE: WARNING ONCE: function "ubifs_remove_from_cat" has inline asm
KLEE: WARNING ONCE: function "ubifs_add_to_cat" has inline asm
KLEE: WARNING ONCE: function "dbg_check_heap" has inline asm
KLEE: WARNING ONCE: function "ubifs_dump_heap" has inline asm
KLEE: WARNING ONCE: function "ubifs_read_nnode" has inline asm
KLEE: WARNING ONCE: function "ubifs_get_pnode" has inline asm
KLEE: WARNING ONCE: function "ubifs_dump_pnode" has inline asm
KLEE: WARNING ONCE: function "check_lpt_type" has inline asm
KLEE: WARNING ONCE: function "ubifs_unpack_bits" has inline asm
KLEE: WARNING ONCE: function "check_lpt_crc" has inline asm
KLEE: WARNING ONCE: function "dirty_cow_nnode" has inline asm
KLEE: WARNING ONCE: function "ubifs_add_lpt_dirt" has inline asm
KLEE: WARNING ONCE: function "ubifs_replace_cat" has inline asm
KLEE: WARNING ONCE: function "fallible_resolve_collision" has inline asm
KLEE: WARNING ONCE: function "resolve_collision" has inline asm
KLEE: WARNING ONCE: function "lnc_add_directly" has inline asm
KLEE: WARNING ONCE: function "fallible_matches_name" has inline asm
KLEE: WARNING ONCE: function "fallible_read_node" has inline asm
KLEE: WARNING ONCE: function "ubifs_wbuf_write_nolock" has inline asm
KLEE: WARNING ONCE: function "ubifs_wbuf_sync_nolock" has inline asm
KLEE: WARNING ONCE: function "ubifs_pad" has inline asm
KLEE: WARNING ONCE: function "ubifs_leb_write" has inline asm
KLEE: WARNING ONCE: function "dbg_leb_write" has inline asm
KLEE: WARNING ONCE: function "power_cut_emulated" has inline asm
KLEE: WARNING ONCE: function "ubifs_dump_leb" has inline asm
KLEE: WARNING ONCE: function "ubifs_scan" has inline asm
KLEE: WARNING ONCE: function "ubifs_start_scan" has inline asm
KLEE: WARNING ONCE: function "ubifs_scan_a_node" has inline asm
KLEE: WARNING ONCE: function "ubifs_end_scan" has inline asm
KLEE: WARNING ONCE: function "ubifs_scanned_corruption" has inline asm
KLEE: WARNING ONCE: function "next_sqnum" has inline asm
KLEE: WARNING ONCE: function "ubifs_find_free_space" has inline asm
KLEE: WARNING ONCE: function "ubifs_garbage_collect" has inline asm
KLEE: WARNING ONCE: function "ubifs_change_one_lp" has inline asm
KLEE: WARNING ONCE: function "ubifs_add_bud_to_log" has inline asm
KLEE: WARNING ONCE: function "ubifs_wbuf_seek_nolock" has inline asm
KLEE: WARNING ONCE: function "ubifs_dump_budg" has inline asm
KLEE: WARNING ONCE: function "ubifs_dump_lprops" has inline asm
KLEE: WARNING ONCE: function "dbg_check_lprops" has inline asm
KLEE: WARNING ONCE: function "scan_check_cb" has inline asm
KLEE: WARNING ONCE: function "ubifs_lpt_scan_nolock" has inline asm
KLEE: WARNING ONCE: function "dbg_check_cats" has inline asm
KLEE: WARNING ONCE: function "scan_get_pnode" has inline asm
KLEE: WARNING ONCE: function "dbg_check_lpt_nodes" has inline asm
KLEE: WARNING ONCE: function "ubifs_tnc_has_node" has inline asm
KLEE: WARNING ONCE: function "lookup_znode" has inline asm
KLEE: WARNING ONCE: function "ubifs_dump_lstats" has inline asm
KLEE: WARNING ONCE: function "ubifs_read_one_lp" has inline asm
KLEE: WARNING ONCE: function "ubifs_get_free_space_nolock" has inline asm
KLEE: WARNING ONCE: function "wait_for_commit" has inline asm
KLEE: WARNING ONCE: function "do_commit" has inline asm
KLEE: WARNING ONCE: function "ubifs_gc_start_commit" has inline asm
KLEE: WARNING ONCE: function "ubifs_log_start_commit" has inline asm
KLEE: WARNING ONCE: function "ubifs_tnc_start_commit" has inline asm
KLEE: WARNING ONCE: function "ubifs_lpt_start_commit" has inline asm
KLEE: WARNING ONCE: function "ubifs_orphan_start_commit" has inline asm
KLEE: WARNING ONCE: function "ubifs_tnc_end_commit" has inline asm
KLEE: WARNING ONCE: function "ubifs_lpt_end_commit" has inline asm
KLEE: WARNING ONCE: function "ubifs_orphan_end_commit" has inline asm
KLEE: WARNING ONCE: function "dbg_check_old_index" has inline asm
KLEE: WARNING ONCE: function "ubifs_write_master" has inline asm
KLEE: WARNING ONCE: function "ubifs_leb_unmap" has inline asm
KLEE: WARNING ONCE: function "lpt_gc" has inline asm
KLEE: WARNING ONCE: function "do_make_pnode_dirty" has inline asm
KLEE: WARNING ONCE: function "ubifs_write_node" has inline asm
KLEE: WARNING ONCE: function "ubifs_prepare_node" has inline asm
KLEE: WARNING ONCE: function "dbg_check_bud_bytes" has inline asm
KLEE: WARNING ONCE: function "ubifs_leb_change" has inline asm
KLEE: WARNING ONCE: function "dbg_orphan_check" has inline asm
KLEE: WARNING ONCE: function "dbg_walk_index" has inline asm
KLEE: WARNING ONCE: function "dbg_chk_lpt_sz" has inline asm
KLEE: WARNING ONCE: function "ubifs_dump_lpt_info" has inline asm
KLEE: WARNING ONCE: function "ubifs_dump_lpt_lebs" has inline asm
KLEE: WARNING ONCE: function "pack_bits" has inline asm
KLEE: WARNING ONCE: function "dbg_chk_lpt_free_spc" has inline asm
KLEE: WARNING ONCE: function "dbg_check_ltab" has inline asm
KLEE: WARNING ONCE: function "upd_ltab" has inline asm
KLEE: WARNING ONCE: function "ubifs_find_free_leb_for_idx" has inline asm
KLEE: WARNING ONCE: function "ubifs_find_dirty_idx_leb" has inline asm
KLEE: WARNING ONCE: function "fill_gap" has inline asm
KLEE: WARNING ONCE: function "ubifs_release_lprops___2" has inline asm
KLEE: WARNING ONCE: function "ubifs_fast_find_empty" has inline asm
KLEE: WARNING ONCE: function "ubifs_fast_find_freeable" has inline asm
KLEE: WARNING ONCE: function "ubifs_fast_find_frdi_idx" has inline asm
KLEE: WARNING ONCE: function "ubifs_leb_map" has inline asm
KLEE: WARNING ONCE: function "ubifs_add_bud" has inline asm
KLEE: WARNING ONCE: function "ubifs_find_dirty_leb" has inline asm
KLEE: WARNING ONCE: function "ubifs_garbage_collect_leb" has inline asm
KLEE: WARNING ONCE: function "switch_gc_head" has inline asm
KLEE: WARNING ONCE: function "dbg_check_data_nodes_order" has inline asm
KLEE: WARNING ONCE: function "dbg_check_nondata_nodes_order" has inline asm
KLEE: WARNING ONCE: function "ubifs_fast_find_free" has inline asm
KLEE: WARNING ONCE: function "can_use_rp" has inline asm
KLEE: WARNING ONCE: function "ubifs_iget" has inline asm
KLEE: WARNING ONCE: function "ubifs_compr_present" has inline asm
KLEE: WARNING ONCE: function "ubifs_compr_name" has inline asm
KLEE: WARNING ONCE: function "dbg_check_dir" has inline asm
KLEE: WARNING ONCE: function "ubifs_dump_inode" has inline asm
KLEE: WARNING ONCE: function "ubifs_tnc_next_ent" has inline asm
KLEE: WARNING ONCE: function "tnc_read_node_nm" has inline asm
KLEE: WARNING ONCE: function "ubifs_new_inode" has inline asm
KLEE: WARNING ONCE: function "ubifs_jnl_update" has inline asm
KLEE: WARNING ONCE: function "ubifs_jnl_change_xattr" has inline asm
KLEE: WARNING ONCE: function "dent_key_init" has inline asm
KLEE: WARNING ONCE: function "ubifs_add_orphan" has inline asm
KLEE: WARNING ONCE: function "ubifs_delete_orphan" has inline asm
KLEE: WARNING ONCE: function "dbg_check_synced_i_size" has inline asm
KLEE: WARNING ONCE: function "do_writepage" has inline asm
KLEE: WARNING ONCE: function "ubifs_jnl_truncate" has inline asm
KLEE: WARNING ONCE: function "data_key_init" has inline asm
KLEE: WARNING ONCE: function "ubifs_decompress" has inline asm
KLEE: WARNING ONCE: function "ubifs_compress" has inline asm
KLEE: WARNING ONCE: function "ubifs_jnl_write_data" has inline asm
KLEE: WARNING ONCE: function "ubifs_ioctl" has inline asm
KLEE: WARNING ONCE: function "ubifs_lookup" has inline asm
KLEE: WARNING ONCE: function "ubifs_create" has inline asm
KLEE: WARNING ONCE: function "ubifs_link" has inline asm
KLEE: WARNING ONCE: function "ubifs_unlink" has inline asm
KLEE: WARNING ONCE: function "ubifs_mkdir" has inline asm
KLEE: WARNING ONCE: function "ubifs_rmdir" has inline asm
KLEE: WARNING ONCE: function "ubifs_rename" has inline asm
KLEE: WARNING ONCE: function "ubifs_jnl_rename" has inline asm
KLEE: WARNING ONCE: function "dent_key_init_flash" has inline asm
KLEE: WARNING ONCE: function "ubifs_readdir" has inline asm
KLEE: WARNING ONCE: function "ubifs_dirty_inode" has inline asm
KLEE: WARNING ONCE: function "ubifs_write_inode" has inline asm
KLEE: WARNING ONCE: function "ubifs_evict_inode" has inline asm
KLEE: WARNING ONCE: function "ubifs_put_super" has inline asm
KLEE: WARNING ONCE: function "ubifs_statfs" has inline asm
KLEE: WARNING ONCE: function "ubifs_remount_fs" has inline asm
KLEE: WARNING ONCE: function "ubifs_parse_options" has inline asm
KLEE: WARNING ONCE: function "dbg_check_space_info" has inline asm
KLEE: WARNING ONCE: function "bu_init" has inline asm
KLEE: WARNING ONCE: function "free_orphans" has inline asm
KLEE: WARNING ONCE: function "ubifs_tnc_close" has inline asm
KLEE: WARNING ONCE: function "ubifs_destroy_tnc_subtree" has inline asm
KLEE: WARNING ONCE: function "ubifs_jnl_delete_inode" has inline asm
KLEE: WARNING ONCE: function "dbg_check_inode_size" has inline asm
KLEE: WARNING ONCE: function "ubifs_vm_page_mkwrite" has inline asm
KLEE: WARNING ONCE: function "shrink_tnc_trees" has inline asm
KLEE: WARNING ONCE: function "ubifs_tnc_levelorder_next" has inline asm
KLEE: WARNING ONCE: function "ubifs_mount" has inline asm
KLEE: WARNING ONCE: function "ubifs_is_mapped" has inline asm
KLEE: WARNING ONCE: function "ubifs_read_superblock" has inline asm
KLEE: WARNING ONCE: function "ubifs_calc_lpt_geom" has inline asm
KLEE: WARNING ONCE: function "ubifs_bg_thread" has inline asm
KLEE: WARNING ONCE: function "ubifs_read_master" has inline asm
KLEE: WARNING ONCE: function "ubifs_recover_inl_heads" has inline asm
KLEE: WARNING ONCE: function "ubifs_fixup_free_space" has inline asm
KLEE: WARNING ONCE: function "dbg_check_idx_size" has inline asm
KLEE: WARNING ONCE: function "ubifs_replay_journal" has inline asm
KLEE: WARNING ONCE: function "ubifs_mount_orphans" has inline asm
KLEE: WARNING ONCE: function "ubifs_consolidate_log" has inline asm
KLEE: WARNING ONCE: function "ubifs_recover_size" has inline asm
KLEE: WARNING ONCE: function "ubifs_rcvry_gc_commit" has inline asm
KLEE: WARNING ONCE: function "take_gc_lnum" has inline asm
KLEE: WARNING ONCE: function "dbg_check_filesystem" has inline asm
KLEE: WARNING ONCE: function "dbg_debugfs_init_fs" has inline asm
KLEE: WARNING ONCE: function "check_leaf" has inline asm
KLEE: WARNING ONCE: function "add_inode" has inline asm
KLEE: WARNING ONCE: function "read_add_inode" has inline asm
KLEE: WARNING ONCE: function "grab_empty_leb" has inline asm
KLEE: WARNING ONCE: function "ubifs_recover_leb" has inline asm
KLEE: WARNING ONCE: function "ubifs_release_lprops___0" has inline asm
KLEE: WARNING ONCE: function "ubifs_recover_log_leb" has inline asm
KLEE: WARNING ONCE: function "fixup_leb" has inline asm
KLEE: WARNING ONCE: function "ubifs_recover_master_node" has inline asm
KLEE: WARNING ONCE: function "ubifs_bg_wbufs_sync" has inline asm
KLEE: WARNING ONCE: function "do_calc_lpt_geom" has inline asm
KLEE: WARNING ONCE: function "ubifs_create_dflt_lpt" has inline asm
KLEE: WARNING ONCE: function "set_ltab" has inline asm
KLEE: WARNING ONCE: function "ubifs_dump_tnc" has inline asm
KLEE: WARNING ONCE: function "do_readpage" has inline asm
KLEE: WARNING ONCE: function "ubifs_tnc_bulk_read" has inline asm
KLEE: WARNING ONCE: function "populate_page" has inline asm
KLEE: WARNING ONCE: function "ubifs_clean_lebs" has inline asm
KLEE: WARNING ONCE: function "ldv_main4_sequence_infinite_withcheck_stateful" has inline asm
KLEE: WARNING ONCE: function "compr_init" has inline asm
KLEE: WARNING ONCE: function "ubifs_dump_sleb" has inline asm
KLEE: WARNING ONCE: function "dbg_debugfs_init" has inline asm
KLEE: WARNING ONCE: flushing 9576 bytes on read, may be slow and/or crash: MO67[9576] allocated at global:
KLEE: ERROR: /tmp/symbiotic-OjHafv/32_7a_cilled_false-unreach-call_linux-3.8-rc1-32_7a-fs--ubifs--ubifs.ko-ldv_main3_sequence_infinite_withcheck_stateful.cil.out.c:10899: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_292ed87b-bcf4-43a9-b251-218a519d4fae/symbiotic/lib/kernel/kfree.c:5: memory error: invalid pointer: free
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-OjHafv/32_7a_cilled_false-unreach-call_linux-3.8-rc1-32_7a-fs--ubifs--ubifs.ko-ldv_main3_sequence_infinite_withcheck_stateful.cil.out.c:12025: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
