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--console--fbcon.ko-entry_point_false-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.: 82 151 2223 14692
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 0.465383052826
Removed calls to 'update_region' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'redraw_screen' (function is undefined)
Removed calls to 'fb_videomode_to_var' (function is undefined)
Defining function fb_get_color_depth as symbolic
Defining function fb_default_cmap as symbolic
Defining function fb_copy_cmap as symbolic
Defining function fb_set_cmap as symbolic
Defining function fb_find_best_mode as symbolic
Defining function fb_set_var as symbolic
Defining function fb_match_mode as symbolic
Defining function vc_resize as symbolic
Defining function get_default_font as symbolic
Defining function find_font as symbolic
Defining function crc32_le as symbolic
Defining function fb_blank as symbolic
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to 'add_timer' (function is undefined)
Removed calls to 'console_unlock' (function is undefined)
Defining function mod_timer as symbolic
Defining function queue_work_on as symbolic
Defining function console_trylock as symbolic
Defining function del_timer_sync as symbolic
Defining function lock_fb_info as symbolic
Defining function fb_notifier_call_chain as symbolic
Defining function printk as symbolic
Removed calls to 'fbcon_set_tileops' (function is undefined)
Removed calls to 'fbcon_set_bitops' (function is undefined)
Defining function fb_show_logo as symbolic
Removed calls to 'console_conditional_schedule' (function is undefined)
Defining function __msecs_to_jiffies as symbolic
Defining function con_is_bound as symbolic
Defining function cancel_work_sync as symbolic
Defining function con_set_default_unimap as symbolic
Defining function con_copy_unimap as symbolic
Removed calls to 'do_blank_screen' (function is undefined)
Removed calls to 'do_unblank_screen' (function is undefined)
Defining function fb_find_nearest_mode as symbolic
Defining function do_take_over_console as symbolic
Defining function do_unregister_con_driver as symbolic
Defining function fb_is_primary_device as symbolic
Defining function do_unbind_con_driver as symbolic
Defining function fb_mode_is_equal as symbolic
Removed calls to 'console_lock' (function is undefined)
Defining function simple_strtoul as symbolic
Defining function snprintf as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'device_remove_file' (function is undefined)
Removed calls to 'device_destroy' (function is undefined)
Defining function fb_register_client as symbolic
Defining function device_create as symbolic
Defining function device_create_file as symbolic
Defining function fb_unregister_client as symbolic
Defining function queue_delayed_work_on as symbolic
Removed calls to 'flush_workqueue' (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.517640113831
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 161 150 1365 8622
INFO: Starting verification
KLEE: WARNING: undefined reference to variable: system_power_efficient_wq
KLEE: ERROR: unable to load symbol(system_power_efficient_wq) while initializing globals.
KLEE: output directory is "/tmp/symbiotic-PiPjpG/klee-out-0"
KLEE: Using STP solver backend
KLEE: WARNING: undefined reference to variable: system_power_efficient_wq
KLEE: ERROR: unable to load symbol(system_power_efficient_wq) while initializing globals.
Running the verifier failed
RESULT: unknown
INFO: Total time elapsed: 1.13123607635
