bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-fs--dlm--dlm.ko-entry_point_true-unreach-call.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.: 739 825 7985 52372
Removed infinite loop in toss_rsb
Removed infinite loop in is_remote
Removed infinite loop in dlm_user_add_ast
Removed infinite loop in dlm_put_lkb
Removed infinite loop in kill_lkb
Removed infinite loop in send_to_sock
Removed infinite loop in queue_cast
Removed infinite loop in add_lkb
Removed infinite loop in add_timeout
Removed infinite loop in unhold_lkb
Removed infinite loop in add_to_waiters
Removed infinite loop in _remove_from_waiters
Removed infinite loop in kill_rsb
Removed infinite loop in recover_locks
Removed infinite loop in unhold_rsb
Removed infinite loop in make_member_array
Removed infinite loop in receive_from_sock
Removed infinite loop in sctp_init_assoc
Removed infinite loop in dlm_process_incoming_buffer
Removed infinite loop in dlm_recovered_lock
Removed infinite loop in sctp_send_shutdown
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 1.64048790932
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'module_put' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'destroy_workqueue' (function is undefined)
Removed calls to 'kmem_cache_free' (function is undefined)
Removed calls to 'kmem_cache_destroy' (function is undefined)
Removed calls to 'sock_release' (function is undefined)
Removed calls to '__free_pages' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Defining function kthread_stop as symbolic
Defining function try_module_get as symbolic
Defining function printk as symbolic
Defining function prepare_to_wait_event as symbolic
Defining function kobject_uevent as symbolic
Defining function debugfs_create_file as symbolic
Defining function snprintf as symbolic
Removed calls to 'debugfs_remove' (function is undefined)
Removed calls to 'down_write' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'flush_workqueue' (function is undefined)
Removed calls to 'up_write' (function is undefined)
Defining function kthread_create_on_node as symbolic
Defining function wake_up_process as symbolic
Defining function kthread_should_stop as symbolic
Removed calls to 'rb_erase' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to 'complete' (function is undefined)
Removed calls to 'down_read' (function is undefined)
Removed calls to 'up_read' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'idr_preload' (function is undefined)
Removed calls to 'idr_remove' (function is undefined)
Defining function jiffies_to_msecs as symbolic
Defining function _cond_resched as symbolic
Removed calls to 'rb_insert_color' (function is undefined)
Removed calls to 'msleep' (function is undefined)
Defining function queue_work_on as symbolic
Defining function ktime_get as symbolic
Defining function rb_first as symbolic
Defining function rb_next as symbolic
Defining function ___ratelimit as symbolic
Defining function debug_lockdep_rcu_enabled as symbolic
Defining function idr_find_slowpath as symbolic
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 '__mutex_init' (function is undefined)
Defining function idr_alloc as symbolic
Defining function jiffies_to_usecs as symbolic
Defining function ns_to_timeval as symbolic
Removed calls to 'finish_wait' (function is undefined)
Defining function schedule_timeout as symbolic
Defining function idr_get_next as symbolic
Defining function __alloc_workqueue_key as symbolic
Defining function vmalloc as symbolic
Defining function kmem_cache_create as symbolic
Defining function schedule_timeout_interruptible as symbolic
Removed calls to 'kfree_skb' (function is undefined)
Defining function netlink_unicast as symbolic
Defining function nla_reserve as symbolic
Defining function genlmsg_put as symbolic
Defining function __alloc_skb as symbolic
Defining function down_read_trylock as symbolic
Removed calls to 'idr_destroy' (function is undefined)
Removed calls to 'vfree' (function is undefined)
Removed calls to 'kobject_put' (function is undefined)
Defining function idr_for_each as symbolic
Defining function misc_deregister as symbolic
Removed calls to 'config_item_put' (function is undefined)
Defining function kstrtoint as symbolic
Defining function sprintf as symbolic
Defining function strcat as symbolic
Defining function capable as symbolic
Defining function kstrtouint as symbolic
Defining function strlcpy as symbolic
Defining function cancel_work_sync as symbolic
Defining function add_uevent_var as symbolic
Defining function noop_llseek as symbolic
Removed calls to 'might_fault' (function is undefined)
Defining function posix_lock_file as symbolic
Defining function _copy_from_user as symbolic
Removed calls to '__copy_to_user_overflow' (function is undefined)
Defining function _copy_to_user as symbolic
Removed calls to 'add_wait_queue' (function is undefined)
Removed calls to 'remove_wait_queue' (function is undefined)
Defining function misc_register as symbolic
Defining function default_wake_function as symbolic
Defining function seq_lseek as symbolic
Defining function seq_read as symbolic
Defining function seq_release as symbolic
Defining function seq_open as symbolic
Defining function default_llseek as symbolic
Defining function simple_open as symbolic
Defining function simple_read_from_buffer as symbolic
Defining function seq_printf as symbolic
Defining function seq_puts as symbolic
Defining function kmem_cache_alloc as symbolic
Removed calls to 'config_group_init' (function is undefined)
Defining function configfs_register_subsystem as symbolic
Removed calls to 'configfs_unregister_subsystem' (function is undefined)
Defining function ldv_probe_23 as symbolic
Defining function ldv_probe_29 as symbolic
Defining function ldv_probe_25 as symbolic
Defining function ldv_probe_27 as symbolic
Defining function pskb_expand_head as symbolic
Defining function skb_clone as symbolic
Defining function skb_copy as symbolic
Defining function __netdev_alloc_skb as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Defining function kset_create_and_add as symbolic
Removed calls to 'kset_unregister' (function is undefined)
Defining function ldv_probe_15 as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'ldv_check_final_state' (function is undefined)
Defining function ldv_open_13 as symbolic
Defining function ldv_release_13 as symbolic
Removed calls to '__init_waitqueue_head' (function is undefined)
Defining function genl_unregister_family as symbolic
Defining function __genl_register_family as symbolic
Defining function debugfs_create_dir as symbolic
Defining function ldv_release_1 as symbolic
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  memcmp
  strlen
  strncmp
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_assume
  __VERIFIER_calloc0
  __VERIFIER_error
  __VERIFIER_exit
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
  __VERIFIER_nondet_loff_t_named
  __VERIFIER_nondet_pointer_named
  __VERIFIER_nondet_size_t_named
  __VERIFIER_nondet_ulong_named
INFO: After-slicing optimizations and preparation time: 1.51072692871
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 832 522 3934 24960
INFO: Starting verification
KLEE: WARNING ONCE: function "dlm_scan_rsbs" has inline asm
KLEE: WARNING ONCE: function "kref_get" has inline asm
KLEE: WARNING ONCE: function "unhold_rsb" has inline asm
KLEE: WARNING ONCE: function "dlm_put_lkb" has inline asm
KLEE: WARNING ONCE: function "__put_lkb" has inline asm
KLEE: WARNING ONCE: function "kill_lkb" has inline asm
KLEE: WARNING ONCE: function "put_rsb" has inline asm
KLEE: WARNING ONCE: function "toss_rsb" has inline asm
KLEE: WARNING ONCE: function "is_remote" has inline asm
KLEE: WARNING ONCE: function "grant_pending_convert" has inline asm
KLEE: WARNING ONCE: function "dlm_lowcomms_commit_buffer" has inline asm
KLEE: WARNING ONCE: function "dlm_user_add_ast" has inline asm
KLEE: WARNING ONCE: function "grant_lock" has inline asm
KLEE: WARNING ONCE: function "queue_cast" has inline asm
KLEE: WARNING ONCE: function "add_lkb" has inline asm
KLEE: WARNING ONCE: function "unhold_lkb" has inline asm
KLEE: WARNING ONCE: function "add_to_waiters" has inline asm
KLEE: WARNING ONCE: function "_remove_from_waiters" has inline asm
KLEE: WARNING ONCE: function "kill_rsb" has inline asm
KLEE: WARNING ONCE: function "dlm_release_lockspace" has inline asm
KLEE: WARNING ONCE: function "validate_lock_args" has inline asm
KLEE: WARNING ONCE: function "add_timeout" has inline asm
KLEE: WARNING ONCE: function "do_unlock" has inline asm
KLEE: WARNING ONCE: function "device_read" has inline asm
KLEE: WARNING ONCE: function "monitor_device_open" has inline asm
KLEE: WARNING ONCE: function "monitor_device_close" has inline asm
KLEE: WARNING ONCE: function "dlm_ls_stop" has inline asm
KLEE: WARNING ONCE: function "table_seq_show" has inline asm
KLEE: WARNING ONCE: function "dlm_recoverd" has inline asm
KLEE: WARNING ONCE: function "dlm_recover_masters" has inline asm
KLEE: WARNING ONCE: function "dlm_recover_locks" has inline asm
KLEE: WARNING ONCE: function "dlm_recover_rsbs" has inline asm
KLEE: WARNING ONCE: function "dlm_callback_resume" has inline asm
KLEE: WARNING ONCE: function "dlm_recover_grant" has inline asm
KLEE: WARNING ONCE: function "_request_lock" has inline asm
KLEE: WARNING ONCE: function "_receive_message" has inline asm
KLEE: WARNING ONCE: function "dlm_master_lookup" has inline asm
KLEE: WARNING ONCE: function "set_new_master" has inline asm
KLEE: WARNING ONCE: function "purge_dead_list" has inline asm
KLEE: WARNING ONCE: function "allow_sync_reply" has inline asm
KLEE: WARNING ONCE: function "disallow_sync_reply" has inline asm
KLEE: WARNING ONCE: function "dlm_callback_suspend" has inline asm
KLEE: WARNING ONCE: function "dlm_lowcomms_connect_node" has inline asm
KLEE: WARNING ONCE: function "dlm_process_incoming_buffer" has inline asm
KLEE: WARNING ONCE: function "receive_sync_reply" has inline asm
KLEE: WARNING ONCE: function "dlm_recovered_lock" has inline asm
KLEE: WARNING ONCE: function "find_rsb" has inline asm
KLEE: WARNING ONCE: function "dlm_lowcomms_close" has inline asm
KLEE: WARNING ONCE: function "dlm_user_purge" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_21" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_19" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_10" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_12" has inline asm
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_e01f69f7-01a7-4840-a812-63f838fb1d4d/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: WARNING: killing 18843 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 44697 states (over memory cap)
KLEE: WARNING: killing 39544 states (over memory cap)
KLEE: WARNING: killing 42029 states (over memory cap)
KLEE: WARNING: killing 39557 states (over memory cap)
KLEE: WARNING: killing 40199 states (over memory cap)
KLEE: WARNING: killing 40548 states (over memory cap)
KLEE: WARNING: killing 44151 states (over memory cap)
KLEE: WARNING: killing 45114 states (over memory cap)
KLEE: WARNING: killing 46791 states (over memory cap)
KLEE: WARNING: killing 46851 states (over memory cap)
KLEE: WARNING: killing 49031 states (over memory cap)
KLEE: WARNING: killing 48063 states (over memory cap)
KLEE: WARNING: killing 47106 states (over memory cap)
KLEE: WARNING: killing 46258 states (over memory cap)
KLEE: WARNING: killing 43459 states (over memory cap)
KLEE: WARNING: killing 44829 states (over memory cap)
KLEE: WARNING: killing 44168 states (over memory cap)
KLEE: WARNING: killing 44174 states (over memory cap)
KLEE: WARNING: killing 45974 states (over memory cap)
KLEE: WARNING: killing 44839 states (over memory cap)
KLEE: WARNING: killing 45501 states (over memory cap)
KLEE: WARNING: killing 45352 states (over memory cap)
KLEE: WARNING: killing 46239 states (over memory cap)
KLEE: WARNING: killing 44942 states (over memory cap)
KLEE: WARNING: killing 46438 states (over memory cap)
KLEE: WARNING: killing 44978 states (over memory cap)
KLEE: WARNING: killing 44866 states (over memory cap)
KLEE: WARNING: killing 44519 states (over memory cap)
KLEE: WARNING: killing 46062 states (over memory cap)
KLEE: WARNING: killing 46600 states (over memory cap)
KLEE: WARNING: killing 44792 states (over memory cap)
KLEE: WARNING: killing 43518 states (over memory cap)
KLEE: WARNING: killing 47300 states (over memory cap)
KLEE: WARNING: killing 44546 states (over memory cap)
KLEE: WARNING: killing 44963 states (over memory cap)
KLEE: WARNING: killing 44913 states (over memory cap)
KLEE: WARNING: killing 43526 states (over memory cap)
KLEE: WARNING: killing 45411 states (over memory cap)
KLEE: WARNING: killing 45779 states (over memory cap)
KLEE: WARNING: killing 44747 states (over memory cap)
KLEE: WARNING: killing 44867 states (over memory cap)
KLEE: WARNING: killing 45808 states (over memory cap)
KLEE: WARNING: killing 46589 states (over memory cap)
KLEE: WARNING: killing 42456 states (over memory cap)
KLEE: WARNING: killing 43058 states (over memory cap)
KLEE: WARNING: killing 45229 states (over memory cap)
KLEE: WARNING: killing 43949 states (over memory cap)
KLEE: WARNING: killing 44425 states (over memory cap)
KLEE: WARNING: killing 47610 states (over memory cap)
KLEE: WARNING: killing 45707 states (over memory cap)
KLEE: WARNING: killing 45537 states (over memory cap)
KLEE: WARNING: killing 45325 states (over memory cap)
KLEE: WARNING: killing 42971 states (over memory cap)
KLEE: WARNING: killing 45152 states (over memory cap)
KLEE: WARNING: killing 44464 states (over memory cap)
KLEE: WARNING: killing 45171 states (over memory cap)
KLEE: WARNING: killing 45400 states (over memory cap)
KLEE: WARNING: killing 44542 states (over memory cap)
KLEE: WARNING: killing 45057 states (over memory cap)
KLEE: WARNING: killing 43682 states (over memory cap)
KLEE: WARNING: killing 45300 states (over memory cap)
KLEE: WARNING: killing 48806 states (over memory cap)
KLEE: WARNING: killing 46776 states (over memory cap)
KLEE: WARNING: killing 45969 states (over memory cap)
KLEE: WARNING: killing 44444 states (over memory cap)
KLEE: WARNING: killing 43727 states (over memory cap)
KLEE: WARNING: killing 44069 states (over memory cap)
KLEE: WARNING: killing 44925 states (over memory cap)
KLEE: WARNING: killing 46191 states (over memory cap)
KLEE: WARNING: killing 45464 states (over memory cap)
KLEE: WARNING: killing 44462 states (over memory cap)
KLEE: WARNING: killing 44805 states (over memory cap)
KLEE: WARNING: killing 45667 states (over memory cap)
KLEE: WARNING: killing 43530 states (over memory cap)
KLEE: WARNING: killing 47607 states (over memory cap)
KLEE: WARNING: killing 45364 states (over memory cap)
KLEE: WARNING: killing 42265 states (over memory cap)
KLEE: WARNING: killing 45769 states (over memory cap)
KLEE: WARNING: killing 47520 states (over memory cap)
KLEE: WARNING: killing 45022 states (over memory cap)
KLEE: WARNING: killing 47558 states (over memory cap)
KLEE: WARNING: killing 44787 states (over memory cap)
KLEE: WARNING: killing 42774 states (over memory cap)
KLEE: WARNING: killing 46750 states (over memory cap)
KLEE: WARNING: killing 42181 states (over memory cap)
KLEE: WARNING: killing 46949 states (over memory cap)
KLEE: WARNING: killing 45341 states (over memory cap)
KLEE: WARNING: killing 44613 states (over memory cap)
KLEE: WARNING: killing 46533 states (over memory cap)
KLEE: WARNING: killing 45890 states (over memory cap)
KLEE: WARNING: killing 44690 states (over memory cap)
KLEE: WARNING: killing 45701 states (over memory cap)
KLEE: WARNING: killing 43769 states (over memory cap)
KLEE: WARNING: killing 44898 states (over memory cap)
KLEE: WARNING: killing 45068 states (over memory cap)
KLEE: WARNING: killing 46570 states (over memory cap)
KLEE: WARNING: killing 46038 states (over memory cap)
