bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.14/linux-3.14__complex_emg__linux-kernel-locking-spinlock__fs-nfs-blocklayout-blocklayoutdriver_true-unreach-call.cil.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.: 282 454 2936 17344
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.707442998886
Removed calls to 'module_put' (function is undefined)
Removed calls to 'lockdep_rcu_suspicious' (function is undefined)
Defining function try_module_get as symbolic
Removed calls to 'dput' (function is undefined)
Defining function rpc_unlink as symbolic
Defining function rpc_d_lookup_sb as symbolic
Defining function rpc_mkpipe_dentry as symbolic
Removed calls to 'lock_acquire' (function is undefined)
Defining function debug_lockdep_rcu_enabled as symbolic
Removed calls to 'lock_release' (function is undefined)
Defining function rcu_is_watching as symbolic
Defining function rcu_lockdep_current_cpu_online as symbolic
Defining function lock_is_held as symbolic
Removed calls to 'rpc_put_sb_net' (function is undefined)
Removed calls to 'rpc_destroy_pipe_data' (function is undefined)
Defining function rpc_get_sb_net as symbolic
Removed calls to '__init_waitqueue_head' (function is undefined)
Defining function rpc_mkpipe_data as symbolic
Removed calls to 'ldv_check_alloc_flags' (function is undefined)
Removed calls to 'ldv_after_alloc' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Defining function printk as symbolic
Removed calls to 'xdr_init_decode_pages' (function is undefined)
Removed calls to 'xdr_set_scratch_buffer' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to '__free_pages' (function is undefined)
Defining function xdr_inline_decode as symbolic
Defining function alloc_pages_current as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'add_wait_queue' (function is undefined)
Removed calls to 'remove_wait_queue' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'blkdev_put' (function is undefined)
Defining function default_wake_function as symbolic
Defining function rpc_queue_upcall as symbolic
Removed calls to '__list_del_entry' (function is undefined)
Defining function xdr_reserve_space as symbolic
Defining function xdr_encode_opaque_fixed as symbolic
Defining function pnfs_generic_pg_readpages as symbolic
Removed calls to 'nfs_pageio_reset_read_mds' (function is undefined)
Removed calls to 'pnfs_generic_pg_init_read' (function is undefined)
Defining function pnfs_generic_pg_test as symbolic
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to 'submit_bio' (function is undefined)
Removed calls to 'pnfs_set_lo_fail' (function is undefined)
Removed calls to 'bio_put' (function is undefined)
Defining function bio_add_page as symbolic
Defining function bio_alloc_bioset as symbolic
Removed calls to '_raw_spin_lock_bh' (function is undefined)
Removed calls to '_raw_spin_unlock_bh' (function is undefined)
Removed calls to 'pnfs_ld_read_done' (function is undefined)
Defining function queue_work_on as symbolic
Defining function nfs4_proc_getdevicelist as symbolic
Defining function nfs4_proc_getdeviceinfo as symbolic
Defining function blkdev_get_by_dev as symbolic
Removed calls to 'unlock_page' (function is undefined)
Removed calls to 'put_page' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'free_buffer_head' (function is undefined)
Removed calls to 'end_page_writeback' (function is undefined)
Removed calls to 'wait_on_page_bit' (function is undefined)
Defining function find_get_page as symbolic
Defining function find_or_create_page as symbolic
Defining function test_set_page_writeback as symbolic
Defining function alloc_page_buffers as symbolic
Defining function bh_uptodate_or_lock as symbolic
Defining function bh_submit_read as symbolic
Removed calls to 'pnfs_ld_write_done' (function is undefined)
Defining function pnfs_generic_pg_writepages as symbolic
Removed calls to 'nfs_pageio_reset_write_mds' (function is undefined)
Removed calls to 'pnfs_generic_pg_init_write' (function is undefined)
Defining function nfs_dreq_bytes_left as symbolic
Defining function radix_tree_next_hole as symbolic
Removed calls to '__wake_up' (function is undefined)
Removed calls to 'might_fault' (function is undefined)
Defining function _copy_from_user as symbolic
Defining function rpc_pipe_generic_upcall as symbolic
Removed calls to 'rpc_pipefs_notifier_unregister' (function is undefined)
Removed calls to 'unregister_pernet_subsys' (function is undefined)
Removed calls to 'pnfs_unregister_layoutdriver' (function is undefined)
Defining function pnfs_register_layoutdriver as symbolic
Defining function register_pernet_subsys as symbolic
Defining function rpc_pipefs_notifier_register as symbolic
Defining function external_allocated_data as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'ldv_assert' (function is undefined)
Linked our definitions to these undefined functions:
  memcmp
  __kmalloc
  kfree
  __VERIFIER_assume
  __VERIFIER_calloc0
  __VERIFIER_error
  __VERIFIER_exit
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
  __VERIFIER_nondet_pointer_named
  __VERIFIER_nondet_ulong_named
INFO: After-slicing optimizations and preparation time: 0.664952039719
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 396 371 1613 9164
INFO: Starting verification
KLEE: WARNING ONCE: function "net_generic" has inline asm
KLEE: WARNING ONCE: function "rcu_read_lock" has inline asm
KLEE: WARNING ONCE: function "rcu_read_unlock" has inline asm
KLEE: WARNING ONCE: function "kref_get" has inline asm
KLEE: WARNING ONCE: function "bl_free_block_dev" has inline asm
KLEE: WARNING ONCE: function "bl_read_pagelist" has inline asm
KLEE: WARNING ONCE: function "zero_user_segments" has inline asm
KLEE: WARNING ONCE: function "bl_end_io_read" has inline asm
KLEE: WARNING ONCE: function "do_add_page_to_bio" has inline asm
KLEE: WARNING ONCE: function "nfs4_blk_decode_device" has inline asm
KLEE: WARNING ONCE: function "bl_write_pagelist" has inline asm
KLEE: WARNING ONCE: function "mark_extents_written" has inline asm
KLEE: WARNING ONCE: function "bl_read_partial_page_sync" has inline asm
KLEE: WARNING ONCE: function "bl_do_readpage_sync" has inline asm
KLEE: WARNING ONCE: function "bl_free_short_extents" has inline asm
KLEE: WARNING: undefined reference to variable: system_wq
KLEE: ERROR: unable to load symbol(system_wq) while initializing globals.
KLEE: output directory is "/tmp/symbiotic-TQALGU/klee-out-0"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: function "net_generic" has inline asm
KLEE: WARNING ONCE: function "rcu_read_lock" has inline asm
KLEE: WARNING ONCE: function "rcu_read_unlock" has inline asm
KLEE: WARNING ONCE: function "kref_get" has inline asm
KLEE: WARNING ONCE: function "bl_free_block_dev" has inline asm
KLEE: WARNING ONCE: function "bl_read_pagelist" has inline asm
KLEE: WARNING ONCE: function "zero_user_segments" has inline asm
KLEE: WARNING ONCE: function "bl_end_io_read" has inline asm
KLEE: WARNING ONCE: function "do_add_page_to_bio" has inline asm
KLEE: WARNING ONCE: function "nfs4_blk_decode_device" has inline asm
KLEE: WARNING ONCE: function "bl_write_pagelist" has inline asm
KLEE: WARNING ONCE: function "mark_extents_written" has inline asm
KLEE: WARNING ONCE: function "bl_read_partial_page_sync" has inline asm
KLEE: WARNING ONCE: function "bl_do_readpage_sync" has inline asm
KLEE: WARNING ONCE: function "bl_free_short_extents" has inline asm
KLEE: WARNING: undefined reference to variable: system_wq
KLEE: ERROR: unable to load symbol(system_wq) while initializing globals.
Running the verifier failed
RESULT: unknown
INFO: Total time elapsed: 1.58971309662
