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--hfs--hfs.ko-ldv_main6_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.: 127 314 2770 21731
Removed infinite loop in hfs_releasepage
Removed infinite loop in hfs_bnode_unhash
Removed infinite loop in hfs_bnode_put
Removed infinite loop in hfs_bnode_create
Removed infinite loop in hfs_test_inode
Removed infinite loop in hfs_btree_open
Removed infinite loop in hfs_write_inode
INFO: Compilation, preparation and instrumentation time: 0.705175161362
Defining function generic_write_end as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function try_to_free_buffers as symbolic
Defining function printk as symbolic
Defining function generic_file_llseek as symbolic
Defining function generic_read_dir as symbolic
Removed calls to '__might_sleep' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to 'mark_page_accessed' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function _atomic_dec_and_lock as symbolic
Removed calls to '__mark_inode_dirty' (function is undefined)
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)
Defining function set_page_dirty as symbolic
Defining function autoremove_wake_function as symbolic
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'put_page' (function is undefined)
Defining function read_cache_page as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'd_instantiate' (function is undefined)
Removed calls to 'd_rehash' (function is undefined)
Removed calls to 'clear_nlink' (function is undefined)
Removed calls to 'iput' (function is undefined)
Removed calls to 'inode_dio_wait' (function is undefined)
Removed calls to 'truncate_setsize' (function is undefined)
Removed calls to 'setattr_copy' (function is undefined)
Defining function inode_change_ok as symbolic
Defining function inode_newsize_ok as symbolic
Removed calls to 'inode_set_bytes' (function is undefined)
Defining function pagecache_write_begin as symbolic
Defining function pagecache_write_end as symbolic
Removed calls to 'panic' (function is undefined)
Defining function msecs_to_jiffies as symbolic
Defining function queue_delayed_work as symbolic
Defining function get_seconds as symbolic
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'set_nlink' (function is undefined)
Removed calls to '__insert_inode_hash' (function is undefined)
Defining function new_inode as symbolic
Defining function debug_lockdep_rcu_enabled as symbolic
Removed calls to 'unlock_new_inode' (function is undefined)
Removed calls to 'make_bad_inode' (function is undefined)
Defining function iget5_locked as symbolic
Removed calls to 'inode_add_bytes' (function is undefined)
Removed calls to 'truncate_pagecache' (function is undefined)
Defining function __blockdev_direct_IO as symbolic
Defining function mpage_writepages as symbolic
Defining function do_sync_read as symbolic
Defining function do_sync_write as symbolic
Defining function generic_file_aio_read as symbolic
Defining function generic_file_aio_write as symbolic
Defining function generic_file_mmap as symbolic
Defining function generic_file_splice_read as symbolic
Defining function filemap_write_and_wait_range as symbolic
Defining function write_inode_now as symbolic
Defining function flush_delayed_work as symbolic
Defining function sync_blockdev as symbolic
Defining function igrab as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to 'init_timer_key' (function is undefined)
Defining function mount_bdev as symbolic
Removed calls to '__brelse' (function is undefined)
Removed calls to 'mark_buffer_dirty' (function is undefined)
Defining function d_make_root as symbolic
Removed calls to 'unload_nls' (function is undefined)
Removed calls to 'free_pages' (function is undefined)
Defining function sb_min_blocksize as symbolic
Defining function sb_set_blocksize as symbolic
Defining function __get_free_pages as symbolic
Defining function sync_dirty_buffer as symbolic
Defining function iget_locked as symbolic
Defining function __bread as symbolic
Defining function ioctl_by_bdev as symbolic
Defining function match_token as symbolic
Defining function match_int as symbolic
Defining function match_octal as symbolic
Defining function match_strdup as symbolic
Defining function load_nls as symbolic
Defining function strsep as symbolic
Defining function load_nls_default as symbolic
Removed calls to 'unlock_buffer' (function is undefined)
Removed calls to '__lock_buffer' (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)
Defining function seq_printf as symbolic
Defining function cancel_delayed_work_sync as symbolic
Removed calls to 'kmem_cache_free' (function is undefined)
Defining function kmem_cache_alloc as symbolic
Defining function generic_block_bmap as symbolic
Defining function cont_write_begin as symbolic
Defining function block_read_full_page as symbolic
Defining function block_write_full_page as symbolic
Defining function mutex_trylock as symbolic
Removed calls to 'ldv_handler_precall' (function is undefined)
Removed calls to 'ldv_check_return_value' (function is undefined)
Removed calls to 'kmem_cache_destroy' (function is undefined)
Removed calls to 'rcu_barrier' (function is undefined)
Defining function unregister_filesystem as symbolic
Removed calls to 'inode_init_once' (function is undefined)
Defining function kmem_cache_create as symbolic
Defining function register_filesystem as symbolic
Linked our definitions to these undefined functions:
  memcmp
  strcmp
  strcpy
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 0.725144147873
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 288 305 1779 15566
INFO: Starting verification
KLEE: WARNING ONCE: function "hfs_releasepage" has inline asm
KLEE: WARNING ONCE: function "hfs_bnode_unhash" has inline asm
KLEE: WARNING ONCE: function "hfs_bnode_put" has inline asm
KLEE: WARNING ONCE: function "hfs_bnode_find" has inline asm
KLEE: WARNING ONCE: function "__hfs_bnode_create" has inline asm
KLEE: WARNING ONCE: function "hfs_bnode_unlink" has inline asm
KLEE: WARNING ONCE: function "hfs_bnode_split" has inline asm
KLEE: WARNING ONCE: function "hfs_extend_file" has inline asm
KLEE: WARNING ONCE: function "hfs_bnode_create" has inline asm
KLEE: WARNING ONCE: function "hfs_vbm_search_free" has inline asm
KLEE: WARNING ONCE: function "hfs_clear_vbm_bits" has inline asm
KLEE: WARNING ONCE: function "hfs_new_inode" has inline asm
KLEE: WARNING ONCE: function "hfs_delete_inode" has inline asm
KLEE: WARNING ONCE: function "hfs_test_inode" has inline asm
KLEE: WARNING ONCE: function "hfs_get_block" has inline asm
KLEE: WARNING ONCE: function "hfs_file_open" has inline asm
KLEE: WARNING ONCE: function "hfs_file_release" has inline asm
KLEE: WARNING ONCE: function "hfs_fill_super" has inline asm
KLEE: WARNING ONCE: function "hfs_btree_open" has inline asm
KLEE: WARNING ONCE: function "hfs_mdb_commit" has inline asm
KLEE: WARNING ONCE: function "lock_buffer" has inline asm
KLEE: WARNING ONCE: function "hfs_write_inode" has inline asm
KLEE: WARNING ONCE: function "hfs_bnode_get" has inline asm
KLEE: WARNING ONCE: function "ldv_main8_sequence_infinite_withcheck_stateful" has inline asm
KLEE: WARNING: undefined reference to function: delayed_work_timer_fn
KLEE: WARNING: undefined reference to function: kill_block_super
KLEE: WARNING: undefined reference to variable: system_long_wq
KLEE: ERROR: unable to load symbol(system_long_wq) while initializing globals.
KLEE: output directory is "/tmp/symbiotic-arBxnz/klee-out-0"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: function "hfs_releasepage" has inline asm
KLEE: WARNING ONCE: function "hfs_bnode_unhash" has inline asm
KLEE: WARNING ONCE: function "hfs_bnode_put" has inline asm
KLEE: WARNING ONCE: function "hfs_bnode_find" has inline asm
KLEE: WARNING ONCE: function "__hfs_bnode_create" has inline asm
KLEE: WARNING ONCE: function "hfs_bnode_unlink" has inline asm
KLEE: WARNING ONCE: function "hfs_bnode_split" has inline asm
KLEE: WARNING ONCE: function "hfs_extend_file" has inline asm
KLEE: WARNING ONCE: function "hfs_bnode_create" has inline asm
KLEE: WARNING ONCE: function "hfs_vbm_search_free" has inline asm
KLEE: WARNING ONCE: function "hfs_clear_vbm_bits" has inline asm
KLEE: WARNING ONCE: function "hfs_new_inode" has inline asm
KLEE: WARNING ONCE: function "hfs_delete_inode" has inline asm
KLEE: WARNING ONCE: function "hfs_test_inode" has inline asm
KLEE: WARNING ONCE: function "hfs_get_block" has inline asm
KLEE: WARNING ONCE: function "hfs_file_open" has inline asm
KLEE: WARNING ONCE: function "hfs_file_release" has inline asm
KLEE: WARNING ONCE: function "hfs_fill_super" has inline asm
KLEE: WARNING ONCE: function "hfs_btree_open" has inline asm
KLEE: WARNING ONCE: function "hfs_mdb_commit" has inline asm
KLEE: WARNING ONCE: function "lock_buffer" has inline asm
KLEE: WARNING ONCE: function "hfs_write_inode" has inline asm
KLEE: WARNING ONCE: function "hfs_bnode_get" has inline asm
KLEE: WARNING ONCE: function "ldv_main8_sequence_infinite_withcheck_stateful" has inline asm
KLEE: WARNING: undefined reference to function: delayed_work_timer_fn
KLEE: WARNING: undefined reference to function: kill_block_super
KLEE: WARNING: undefined reference to variable: system_long_wq
KLEE: ERROR: unable to load symbol(system_long_wq) while initializing globals.
Running the verifier failed
RESULT: unknown
INFO: Total time elapsed: 1.65915513039
