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-alloc-spinlock__fs-nfs-nfs_layout_nfsv41_files_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.: 238 405 2453 13859
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.609436035156
Defining function printk as symbolic
Defining function nfs41_sequence_done as symbolic
Removed calls to 'rpc_exit' (function is undefined)
Defining function nfs41_setup_sequence as symbolic
Defining function nfs4_set_rw_stateid as symbolic
Removed calls to 'nfs_remove_bad_delegation' (function is undefined)
Removed calls to 'nfs4_schedule_lease_recovery' (function is undefined)
Removed calls to 'nfs4_schedule_session_recovery' (function is undefined)
Removed calls to 'rpc_delay' (function is undefined)
Removed calls to 'pnfs_destroy_layout' (function is undefined)
Removed calls to 'rpc_wake_up' (function is undefined)
Removed calls to 'nfs4_mark_deviceid_unavailable' (function is undefined)
Removed calls to 'rpc_sleep_on' (function is undefined)
Removed calls to 'rpc_wake_up_queued_task' (function is undefined)
Defining function rpc_restart_call_prepare as symbolic
Defining function nfs4_schedule_stateid_recovery as symbolic
Defining function pnfs_read_done_resend_to_mds as symbolic
Defining function nfs4_test_deviceid_unavailable as symbolic
Removed calls to 'rpc_count_iostats' (function is undefined)
Removed calls to 'nfs_put_client' (function is undefined)
Defining function pnfs_write_done_resend_to_mds as symbolic
Removed calls to 'pnfs_put_lseg' (function is undefined)
Removed calls to 'nfs_commitdata_release' (function is undefined)
Removed calls to 'ldv_after_alloc' (function is undefined)
Removed calls to 'xdr_init_decode_pages' (function is undefined)
Removed calls to 'xdr_set_scratch_buffer' (function is undefined)
Removed calls to 'nfs4_print_deviceid' (function is undefined)
Removed calls to '__free_pages' (function is undefined)
Defining function nfs4_find_get_deviceid as symbolic
Removed calls to 'nfs4_init_deviceid_node' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to 'ldv_assert' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Defining function nfs4_put_deviceid_node as symbolic
Defining function nfs4_proc_getdeviceinfo as symbolic
Defining function nfs4_insert_deviceid_node as symbolic
Defining function __ldv_atomic_dec_and_lock as symbolic
Defining function xdr_inline_decode as symbolic
Defining function __ipv6_addr_type as symbolic
Defining function rpc_pton as symbolic
Defining function sscanf as symbolic
Defining function snprintf as symbolic
Defining function external_allocated_data as symbolic
Removed calls to 'nfs_request_remove_commit_list' (function is undefined)
Removed calls to 'nfs_retry_commit' (function is undefined)
Removed calls to 'nfs_init_commit' (function is undefined)
Defining function nfs_commitdata_alloc as symbolic
Defining function nfs_initiate_commit as symbolic
Removed calls to 'wake_up_bit' (function is undefined)
Defining function nfs4_find_or_create_ds_client as symbolic
Defining function nfs4_set_ds_client as symbolic
Defining function nfs4_init_ds_session as symbolic
Removed calls to 'nfs_request_add_commit_list' (function is undefined)
Defining function pnfs_generic_pg_readpages as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'nfs_pageio_reset_read_mds' (function is undefined)
Defining function pnfs_update_layout as symbolic
Defining function pnfs_generic_pg_test as symbolic
Defining function nfs_generic_pg_test as symbolic
Defining function nfs_initiate_read as symbolic
Removed calls to '__might_sleep' (function is undefined)
Defining function __cond_resched_lock as symbolic
Removed calls to 'pnfs_set_layoutcommit' (function is undefined)
Defining function nfs_initiate_write as symbolic
Defining function pnfs_generic_pg_writepages as symbolic
Removed calls to 'nfs_init_cinfo' (function is undefined)
Removed calls to 'nfs_pageio_reset_write_mds' (function is undefined)
Removed calls to 'pnfs_unregister_layoutdriver' (function is undefined)
Defining function pnfs_register_layoutdriver as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Linked our definitions to these undefined functions:
  strlen
  strncmp
  strrchr
  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.602141857147
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 330 343 1073 7387
INFO: Starting verification
KLEE: WARNING ONCE: function "filelayout_async_handle_error" has inline asm
KLEE: WARNING ONCE: function "filelayout_commit_pagelist" has inline asm
KLEE: WARNING ONCE: function "nfs4_fl_prepare_ds" has inline asm
KLEE: WARNING ONCE: function "filelayout_mark_request_commit" has inline asm
KLEE: WARNING ONCE: function "filelayout_read_pagelist" has inline asm
KLEE: WARNING ONCE: function "filelayout_get_dserver_offset" has inline asm
KLEE: WARNING ONCE: function "transfer_commit_list" has inline asm
KLEE: WARNING ONCE: function "filelayout_scan_commit_lists" has inline asm
KLEE: WARNING ONCE: function "filelayout_write_pagelist" has inline asm
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_4ef7bf2c-ac7f-4aca-8fb4-b047f627a0ab/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_4ef7bf2c-ac7f-4aca-8fb4-b047f627a0ab/symbiotic/lib/kernel/kfree.c:5: memory error: invalid pointer: free
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_4ef7bf2c-ac7f-4aca-8fb4-b047f627a0ab/symbiotic/lib/kernel/kfree.c:5: free of global
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-jmLqW6/linux-3.14__complex_emg__linux-alloc-spinlock__fs-nfs-nfs_layout_nfsv41_files_true-unreach-call.cil.c:10716: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-jmLqW6/linux-3.14__complex_emg__linux-alloc-spinlock__fs-nfs-nfs_layout_nfsv41_files_true-unreach-call.cil.c:9442: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-jmLqW6/linux-3.14__complex_emg__linux-alloc-spinlock__fs-nfs-nfs_layout_nfsv41_files_true-unreach-call.cil.c:9443: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
