bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--video--fbdev--core--fb.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.: 263 296 2978 21624
Removed infinite loop in fb_deferred_io_init
Removed infinite loop in fb_deferred_io_cleanup
Removed infinite loop in fb_deferred_io_fault
Removed infinite loop in get_page
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 0.705359220505
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function fb_find_logo as symbolic
Defining function __bitmap_weight as symbolic
Defining function fb_notifier_call_chain as symbolic
Removed calls to 'list_del' (function is undefined)
Defining function printk as symbolic
Removed calls to '__list_add' (function is undefined)
Removed calls to 'device_destroy' (function is undefined)
Removed calls to 'console_lock' (function is undefined)
Removed calls to 'console_unlock' (function is undefined)
Removed calls to 'pm_vt_switch_unregister' (function is undefined)
Removed calls to 'device_remove_file' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'pm_vt_switch_required' (function is undefined)
Defining function fb_is_primary_device as symbolic
Defining function device_create as symbolic
Defining function device_create_file as symbolic
Defining function of_get_videomode as symbolic
Defining function __memmove as symbolic
Defining function int_sqrt as symbolic
Defining function simple_strtol as symbolic
Defining function snprintf as symbolic
Defining function filemap_write_and_wait_range as symbolic
Defining function queue_delayed_work_on as symbolic
Defining function cancel_delayed_work_sync as symbolic
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)
Removed calls to 'unlock_page' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to '__lock_page' (function is undefined)
Defining function page_mkclean as symbolic
Removed calls to 'mutex_destroy' (function is undefined)
Defining function vmalloc_to_page 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
Removed calls to '__might_fault' (function is undefined)
Defining function __request_module as symbolic
Defining function vm_get_page_prot as symbolic
Defining function vm_iomap_memory as symbolic
Defining function compat_alloc_user_space as symbolic
Defining function copy_in_user as symbolic
Removed calls to '__copy_to_user_overflow' (function is undefined)
Defining function _copy_to_user as symbolic
Removed calls to '__copy_from_user_overflow' (function is undefined)
Defining function _copy_from_user as symbolic
Defining function seq_printf as symbolic
Defining function sscanf as symbolic
Defining function simple_strtoul as symbolic
Removed calls to 'dump_page' (function is undefined)
Defining function file_update_time as symbolic
Defining function __get_page_tail as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'remove_proc_entry' (function is undefined)
Removed calls to 'class_destroy' (function is undefined)
Removed calls to '__unregister_chrdev' (function is undefined)
Defining function ldv_release_3 as symbolic
Defining function ldv_probe_3 as symbolic
Defining function __class_create as symbolic
Defining function __register_chrdev as symbolic
Defining function proc_create_data as symbolic
Defining function queue_work_on as symbolic
Removed calls to 'flush_workqueue' (function is undefined)
Linked our definitions to these undefined functions:
  memcmp
  strlen
  strncmp
  __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.787869930267
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 360 251 1664 13471
INFO: Starting verification
KLEE: WARNING ONCE: function "put_fb_info" has inline asm
KLEE: WARNING ONCE: function "fb_deferred_io_init" has inline asm
KLEE: WARNING ONCE: function "lock_page" has inline asm
KLEE: WARNING ONCE: function "fb_deferred_io_cleanup" has inline asm
KLEE: WARNING ONCE: function "fb_compat_ioctl" has inline asm
KLEE: WARNING ONCE: function "get_fb_info" has inline asm
KLEE: WARNING ONCE: function "fb_deferred_io_fault" has inline asm
KLEE: WARNING ONCE: function "fb_deferred_io_set_page_dirty" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_2" has inline asm
KLEE: WARNING: undefined reference to function: delayed_work_timer_fn
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-VPatb1/klee-out-0"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: function "put_fb_info" has inline asm
KLEE: WARNING ONCE: function "fb_deferred_io_init" has inline asm
KLEE: WARNING ONCE: function "lock_page" has inline asm
KLEE: WARNING ONCE: function "fb_deferred_io_cleanup" has inline asm
KLEE: WARNING ONCE: function "fb_compat_ioctl" has inline asm
KLEE: WARNING ONCE: function "get_fb_info" has inline asm
KLEE: WARNING ONCE: function "fb_deferred_io_fault" has inline asm
KLEE: WARNING ONCE: function "fb_deferred_io_set_page_dirty" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_2" has inline asm
KLEE: WARNING: undefined reference to function: delayed_work_timer_fn
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.70547413826
