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--ecryptfs--ecryptfs.ko-ldv_main1_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.: 539 672 4252 28761
Removed infinite loop in sg_assign_page
Removed infinite loop in ecryptfs_tfm_exists
Removed infinite loop in ecryptfs_add_new_key_tfm
Removed infinite loop in ecryptfs_compute_root_iv
Removed infinite loop in ecryptfs_parse_packet_set
Removed infinite loop in ecryptfs_write_inode_size_to_metadata
Removed infinite loop in ecryptfs_encrypt_page
Removed infinite loop in encrypt_scatterlist
Removed infinite loop in ecryptfs_lookup_interpose
Removed infinite loop in ecryptfs_destroy_inode
Removed infinite loop in zero_user_segments
Removed infinite loop in ecryptfs_decrypt_page
Removed infinite loop in ecryptfs_parse_options
Removed infinite loop in ecryptfs_miscdev_read
Removed infinite loop in ecryptfs_miscdev_release
Removed infinite loop in ecryptfs_destroy_ecryptfs_miscdev
INFO: Compilation, preparation and instrumentation time: 1.2792570591
Removed calls to 'fsstack_copy_attr_all' (function is undefined)
Removed calls to 'dput' (function is undefined)
Removed calls to 'mntput' (function is undefined)
Removed calls to 'kmem_cache_free' (function is undefined)
Defining function default_llseek as symbolic
Defining function generic_read_dir as symbolic
Defining function generic_file_splice_read as symbolic
Defining function vfs_fsync as symbolic
Removed calls to 'fput' (function is undefined)
Defining function filemap_write_and_wait as symbolic
Removed calls to 'mutex_unlock' (function is undefined)
Defining function atomic_dec_and_mutex_lock as symbolic
Defining function printk as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'get_random_bytes' (function is undefined)
Removed calls to 'free_pages' (function is undefined)
Removed calls to '__mark_inode_dirty' (function is undefined)
Defining function vfs_write as symbolic
Defining function vfs_setxattr as symbolic
Removed calls to 'up_write' (function is undefined)
Removed calls to 'key_put' (function is undefined)
Defining function kmem_cache_alloc as symbolic
Removed calls to 'down_write' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Defining function schedule_timeout_interruptible as symbolic
Removed calls to '__wake_up' (function is undefined)
Defining function mutex_trylock as symbolic
Defining function debug_lockdep_rcu_enabled as symbolic
Defining function simple_strtol as symbolic
Removed calls to 'sg_init_table' (function is undefined)
Defining function __phys_addr as symbolic
Removed calls to '__mutex_init' (function is undefined)
Defining function crypto_alloc_base as symbolic
Defining function snprintf as symbolic
Defining function key_validate as symbolic
Defining function alloc_pages_current as symbolic
Removed calls to 'sg_init_one' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Defining function request_key as symbolic
Defining function sprintf as symbolic
Defining function vfs_read as symbolic
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'wait_for_completion' (function is undefined)
Defining function dentry_open as symbolic
Defining function vprintk as symbolic
Defining function vfs_readdir as symbolic
Defining function generic_file_llseek as symbolic
Defining function do_sync_read as symbolic
Defining function do_sync_write as symbolic
Removed calls to 'touch_atime' (function is undefined)
Defining function generic_file_aio_write as symbolic
Defining function generic_file_mmap as symbolic
Defining function generic_file_aio_read as symbolic
Defining function wait_on_sync_kiocb as symbolic
Defining function generic_readlink as symbolic
Removed calls to 'generic_fillattr' (function is undefined)
Defining function inode_change_ok as symbolic
Removed calls to 'truncate_setsize' (function is undefined)
Defining function notify_change 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 '__lock_page' (function is undefined)
Removed calls to '__free_pages' (function is undefined)
Defining function read_cache_page as symbolic
Defining function inode_newsize_ok as symbolic
Defining function inode_permission as symbolic
Removed calls to 'd_instantiate' (function is undefined)
Removed calls to 'd_rehash' (function is undefined)
Removed calls to 'make_bad_inode' (function is undefined)
Removed calls to 'unlock_new_inode' (function is undefined)
Removed calls to 'fsstack_copy_inode_size' (function is undefined)
Removed calls to 'iput' (function is undefined)
Removed calls to 'set_nlink' (function is undefined)
Removed calls to 'd_drop' (function is undefined)
Removed calls to 'clear_nlink' (function is undefined)
Removed calls to 'unlock_rename' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function dget_parent as symbolic
Defining function lock_rename as symbolic
Defining function vfs_rename as symbolic
Defining function vfs_mknod as symbolic
Defining function igrab as symbolic
Removed calls to 'init_special_inode' (function is undefined)
Defining function iget5_locked as symbolic
Removed calls to 'mutex_lock_nested' (function is undefined)
Defining function vfs_rmdir as symbolic
Defining function vfs_mkdir as symbolic
Defining function vfs_symlink as symbolic
Removed calls to 'kzfree' (function is undefined)
Defining function vfs_unlink as symbolic
Defining function vfs_link as symbolic
Defining function vfs_create as symbolic
Defining function lookup_one_len as symbolic
Defining function mntget as symbolic
Defining function vfs_getattr as symbolic
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 grab_cache_page_write_begin as symbolic
Removed calls to 'inode_init_once' (function is undefined)
Removed calls to 'path_put' (function is undefined)
Removed calls to 'deactivate_locked_super' (function is undefined)
Removed calls to 'kill_anon_super' (function is undefined)
Removed calls to 'bdi_destroy' (function is undefined)
Defining function set_anon_super as symbolic
Defining function sget as symbolic
Defining function bdi_setup_and_register as symbolic
Defining function kern_path as symbolic
Defining function d_make_root as symbolic
Defining function match_token as symbolic
Defining function strsep as symbolic
Defining function noop_llseek 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 'might_fault' (function is undefined)
Removed calls to 'module_put' (function is undefined)
Defining function try_module_get as symbolic
Defining function memdup_user as symbolic
Defining function wake_up_process as symbolic
Defining function _copy_from_user as symbolic
Defining function autoremove_wake_function as symbolic
Defining function _copy_to_user as symbolic
Removed calls to 'ldv_handler_precall' (function is undefined)
Removed calls to 'ldv_check_return_value' (function is undefined)
Removed calls to 'kobject_put' (function is undefined)
Removed calls to 'sysfs_remove_group' (function is undefined)
Removed calls to 'complete' (function is undefined)
Defining function unregister_filesystem as symbolic
Removed calls to 'rcu_barrier' (function is undefined)
Removed calls to 'kmem_cache_destroy' (function is undefined)
Defining function kthread_stop as symbolic
Defining function misc_deregister as symbolic
Defining function register_filesystem as symbolic
Defining function misc_register 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 kobject_create_and_add as symbolic
Defining function sysfs_create_group as symbolic
Defining function kmem_cache_create as symbolic
Linked our definitions to these undefined functions:
  memcmp
  strcmp
  strcpy
  strlen
  strncmp
  strncpy
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 1.26026892662
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 791 556 3029 17090
INFO: Starting verification
KLEE: WARNING ONCE: function "ecryptfs_get_lower_file" has inline asm
KLEE: WARNING ONCE: function "ecryptfs_write_metadata" has inline asm
KLEE: WARNING ONCE: function "ecryptfs_write_lower" has inline asm
KLEE: WARNING ONCE: function "ecryptfs_send_message" has inline asm
KLEE: WARNING ONCE: function "ecryptfs_find_global_auth_tok_for_sig" has inline asm
KLEE: WARNING ONCE: function "ecryptfs_find_daemon_by_euid" has inline asm
KLEE: WARNING ONCE: function "sg_set_page" has inline asm
KLEE: WARNING ONCE: function "ecryptfs_tfm_exists" has inline asm
KLEE: WARNING ONCE: function "ecryptfs_add_new_key_tfm" has inline asm
KLEE: WARNING ONCE: function "ecryptfs_compute_root_iv" has inline asm
KLEE: WARNING ONCE: function "ecryptfs_read_lower" has inline asm
KLEE: WARNING ONCE: function "ecryptfs_parse_packet_set" has inline asm
KLEE: WARNING ONCE: function "ecryptfs_readlink_lower" has inline asm
KLEE: WARNING ONCE: function "ecryptfs_write" has inline asm
KLEE: WARNING ONCE: function "ecryptfs_write_inode_size_to_metadata" has inline asm
KLEE: WARNING ONCE: function "ecryptfs_get_locked_page" has inline asm
KLEE: WARNING ONCE: function "ecryptfs_encrypt_page" has inline asm
KLEE: WARNING ONCE: function "ecryptfs_lookup" has inline asm
KLEE: WARNING ONCE: function "ecryptfs_destroy_inode" has inline asm
KLEE: WARNING ONCE: function "ecryptfs_writepage" has inline asm
KLEE: WARNING ONCE: function "ecryptfs_readpage" has inline asm
KLEE: WARNING ONCE: function "ecryptfs_write_begin" has inline asm
KLEE: WARNING ONCE: function "ecryptfs_write_end" has inline asm
KLEE: WARNING ONCE: function "ecryptfs_copy_up_encrypted_with_header" has inline asm
KLEE: WARNING ONCE: function "ecryptfs_decrypt_page" has inline asm
KLEE: WARNING ONCE: function "ecryptfs_mount" has inline asm
KLEE: WARNING ONCE: function "ecryptfs_miscdev_read" has inline asm
KLEE: WARNING ONCE: function "ecryptfs_miscdev_open" has inline asm
KLEE: WARNING ONCE: function "ecryptfs_miscdev_release" has inline asm
KLEE: WARNING ONCE: function "ecryptfs_spawn_daemon" has inline asm
KLEE: WARNING ONCE: function "ecryptfs_destroy_ecryptfs_miscdev" has inline asm
KLEE: WARNING ONCE: function "ecryptfs_threadfn" has inline asm
KLEE: WARNING: undefined reference to variable: key_type_encrypted
KLEE: WARNING: undefined reference to variable: key_type_user
KLEE: WARNING: Type for key_type_encrypted is not sized
KLEE: WARNING: Unable to find size for global variable: key_type_encrypted (use will result in out of bounds access)
KLEE: WARNING: Type for key_type_user is not sized
KLEE: WARNING: Unable to find size for global variable: key_type_user (use will result in out of bounds access)
KLEE: WARNING ONCE: flushing 9576 bytes on read, may be slow and/or crash: MO180[9576] allocated at global:
KLEE: ERROR: /tmp/symbiotic-xo08uN/32_7a_cilled_false-unreach-call_linux-3.8-rc1-32_7a-fs--ecryptfs--ecryptfs.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:4342: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xo08uN/32_7a_cilled_false-unreach-call_linux-3.8-rc1-32_7a-fs--ecryptfs--ecryptfs.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:4342: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xo08uN/32_7a_cilled_false-unreach-call_linux-3.8-rc1-32_7a-fs--ecryptfs--ecryptfs.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:4325: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xo08uN/32_7a_cilled_false-unreach-call_linux-3.8-rc1-32_7a-fs--ecryptfs--ecryptfs.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:4325: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xo08uN/32_7a_cilled_false-unreach-call_linux-3.8-rc1-32_7a-fs--ecryptfs--ecryptfs.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:4342: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xo08uN/32_7a_cilled_false-unreach-call_linux-3.8-rc1-32_7a-fs--ecryptfs--ecryptfs.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:4342: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xo08uN/32_7a_cilled_false-unreach-call_linux-3.8-rc1-32_7a-fs--ecryptfs--ecryptfs.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:4551: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xo08uN/32_7a_cilled_false-unreach-call_linux-3.8-rc1-32_7a-fs--ecryptfs--ecryptfs.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:4342: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xo08uN/32_7a_cilled_false-unreach-call_linux-3.8-rc1-32_7a-fs--ecryptfs--ecryptfs.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:4342: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xo08uN/32_7a_cilled_false-unreach-call_linux-3.8-rc1-32_7a-fs--ecryptfs--ecryptfs.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:4325: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xo08uN/32_7a_cilled_false-unreach-call_linux-3.8-rc1-32_7a-fs--ecryptfs--ecryptfs.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:4325: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xo08uN/32_7a_cilled_false-unreach-call_linux-3.8-rc1-32_7a-fs--ecryptfs--ecryptfs.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:4342: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xo08uN/32_7a_cilled_false-unreach-call_linux-3.8-rc1-32_7a-fs--ecryptfs--ecryptfs.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:4342: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xo08uN/32_7a_cilled_false-unreach-call_linux-3.8-rc1-32_7a-fs--ecryptfs--ecryptfs.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:4342: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xo08uN/32_7a_cilled_false-unreach-call_linux-3.8-rc1-32_7a-fs--ecryptfs--ecryptfs.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:4342: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xo08uN/32_7a_cilled_false-unreach-call_linux-3.8-rc1-32_7a-fs--ecryptfs--ecryptfs.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:4342: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xo08uN/32_7a_cilled_false-unreach-call_linux-3.8-rc1-32_7a-fs--ecryptfs--ecryptfs.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:4552: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xo08uN/32_7a_cilled_false-unreach-call_linux-3.8-rc1-32_7a-fs--ecryptfs--ecryptfs.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:4342: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xo08uN/32_7a_cilled_false-unreach-call_linux-3.8-rc1-32_7a-fs--ecryptfs--ecryptfs.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:4342: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xo08uN/32_7a_cilled_false-unreach-call_linux-3.8-rc1-32_7a-fs--ecryptfs--ecryptfs.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:4342: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xo08uN/32_7a_cilled_false-unreach-call_linux-3.8-rc1-32_7a-fs--ecryptfs--ecryptfs.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:4444: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
