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_true-unreach-call_linux-3.8-rc1-drivers--block--paride--pg.ko-main.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.: 68 75 587 2823
INFO: Compilation, preparation and instrumentation time: 0.192702054977
Removed calls to 'device_destroy' (function is undefined)
Removed calls to 'class_destroy' (function is undefined)
Removed calls to '__unregister_chrdev' (function is undefined)
Removed calls to 'pi_release' (function is undefined)
Removed calls to 'might_fault' (function is undefined)
Defining function noop_llseek as symbolic
Defining function printk as symbolic
Defining function __class_create as symbolic
Defining function device_create as symbolic
Defining function __register_chrdev as symbolic
Defining function pi_init as symbolic
Removed calls to 'pi_connect' (function is undefined)
Removed calls to 'pi_write_regr' (function is undefined)
Removed calls to 'pi_disconnect' (function is undefined)
Removed calls to 'pi_write_block' (function is undefined)
Removed calls to 'pi_read_block' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Defining function pi_read_regr as symbolic
Defining function schedule_timeout_interruptible as symbolic
Defining function snprintf as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function _copy_to_user as symbolic
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Defining function _copy_from_user as symbolic
Defining function mutex_trylock as symbolic
Linked our definitions to these undefined functions:
  memcmp
  __kmalloc
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 0.167869091034
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 105 73 362 1721
INFO: Starting verification
KLEE: WARNING ONCE: function "main" has inline asm
KLEE: WARNING ONCE: function "pg_open" has inline asm
KLEE: WARNING ONCE: function "pg_release" has inline asm
KLEE: ERROR: /tmp/symbiotic-gVDw14/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--block--paride--pg.ko-main.cil.out.c:2803: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16501 states (over memory cap)
KLEE: WARNING: killing 12438 states (over memory cap)
KLEE: WARNING: killing 12025 states (over memory cap)
KLEE: WARNING: killing 12198 states (over memory cap)
KLEE: WARNING: killing 12371 states (over memory cap)
KLEE: WARNING: killing 12090 states (over memory cap)
KLEE: WARNING: killing 12152 states (over memory cap)
KLEE: WARNING: killing 12438 states (over memory cap)
KLEE: WARNING: killing 12275 states (over memory cap)
KLEE: WARNING: killing 12231 states (over memory cap)
KLEE: WARNING: killing 12297 states (over memory cap)
KLEE: WARNING: killing 12472 states (over memory cap)
KLEE: WARNING: killing 12203 states (over memory cap)
KLEE: WARNING: killing 12713 states (over memory cap)
KLEE: WARNING: killing 12223 states (over memory cap)
KLEE: WARNING: killing 12394 states (over memory cap)
KLEE: WARNING: killing 12243 states (over memory cap)
KLEE: WARNING: killing 12198 states (over memory cap)
KLEE: WARNING: killing 12589 states (over memory cap)
KLEE: WARNING: killing 12214 states (over memory cap)
KLEE: WARNING: killing 12605 states (over memory cap)
KLEE: WARNING: killing 12348 states (over memory cap)
KLEE: WARNING: killing 12298 states (over memory cap)
KLEE: WARNING: killing 12364 states (over memory cap)
KLEE: WARNING: killing 12322 states (over memory cap)
KLEE: WARNING: killing 11957 states (over memory cap)
KLEE: WARNING: killing 12229 states (over memory cap)
KLEE: WARNING: killing 12294 states (over memory cap)
KLEE: WARNING: killing 12258 states (over memory cap)
KLEE: WARNING: killing 12108 states (over memory cap)
KLEE: WARNING: killing 12279 states (over memory cap)
KLEE: WARNING: killing 12244 states (over memory cap)
KLEE: WARNING: killing 12204 states (over memory cap)
KLEE: WARNING: killing 12268 states (over memory cap)
KLEE: WARNING: killing 12127 states (over memory cap)
KLEE: WARNING: killing 12189 states (over memory cap)
KLEE: WARNING: killing 12258 states (over memory cap)
KLEE: WARNING: killing 12018 states (over memory cap)
KLEE: WARNING: killing 12086 states (over memory cap)
KLEE: WARNING: killing 12249 states (over memory cap)
KLEE: WARNING: killing 12104 states (over memory cap)
KLEE: WARNING: killing 12175 states (over memory cap)
KLEE: WARNING: killing 12137 states (over memory cap)
KLEE: WARNING: killing 12201 states (over memory cap)
KLEE: WARNING: killing 11970 states (over memory cap)
KLEE: WARNING: killing 12134 states (over memory cap)
KLEE: WARNING: killing 11799 states (over memory cap)
KLEE: WARNING: killing 12261 states (over memory cap)
KLEE: WARNING: killing 12028 states (over memory cap)
KLEE: WARNING: killing 12093 states (over memory cap)
KLEE: WARNING: killing 12059 states (over memory cap)
KLEE: WARNING: killing 12026 states (over memory cap)
KLEE: WARNING: killing 11992 states (over memory cap)
KLEE: WARNING: killing 11962 states (over memory cap)
KLEE: WARNING: killing 12022 states (over memory cap)
KLEE: WARNING: killing 11894 states (over memory cap)
KLEE: WARNING: killing 11962 states (over memory cap)
KLEE: WARNING: killing 12028 states (over memory cap)
KLEE: WARNING: killing 12093 states (over memory cap)
KLEE: WARNING: killing 12157 states (over memory cap)
KLEE: WARNING: killing 12032 states (over memory cap)
KLEE: WARNING: killing 11908 states (over memory cap)
KLEE: WARNING: killing 11975 states (over memory cap)
KLEE: WARNING: killing 11848 states (over memory cap)
KLEE: WARNING: killing 12105 states (over memory cap)
KLEE: WARNING: killing 12260 states (over memory cap)
KLEE: WARNING: killing 11849 states (over memory cap)
KLEE: WARNING: killing 11822 states (over memory cap)
KLEE: WARNING: killing 11793 states (over memory cap)
KLEE: WARNING: killing 11762 states (over memory cap)
KLEE: WARNING: killing 12014 states (over memory cap)
KLEE: WARNING: killing 11886 states (over memory cap)
KLEE: WARNING: killing 11952 states (over memory cap)
KLEE: WARNING: killing 12115 states (over memory cap)
KLEE: WARNING: killing 11902 states (over memory cap)
KLEE: WARNING: killing 11782 states (over memory cap)
KLEE: WARNING: killing 12123 states (over memory cap)
KLEE: WARNING: killing 11909 states (over memory cap)
KLEE: WARNING: killing 12060 states (over memory cap)
KLEE: WARNING: killing 11849 states (over memory cap)
KLEE: WARNING: killing 11821 states (over memory cap)
KLEE: WARNING: killing 11980 states (over memory cap)
KLEE: WARNING: killing 11764 states (over memory cap)
KLEE: WARNING: killing 11827 states (over memory cap)
KLEE: WARNING: killing 11890 states (over memory cap)
KLEE: WARNING: killing 11857 states (over memory cap)
KLEE: WARNING: killing 11836 states (over memory cap)
KLEE: WARNING: killing 12078 states (over memory cap)
KLEE: WARNING: killing 11784 states (over memory cap)
KLEE: WARNING: killing 11849 states (over memory cap)
KLEE: WARNING: killing 11822 states (over memory cap)
KLEE: WARNING: killing 11973 states (over memory cap)
KLEE: WARNING: killing 11945 states (over memory cap)
KLEE: WARNING: killing 11731 states (over memory cap)
KLEE: WARNING: killing 11701 states (over memory cap)
KLEE: WARNING: killing 11768 states (over memory cap)
KLEE: WARNING: killing 11824 states (over memory cap)
KLEE: WARNING: killing 11888 states (over memory cap)
KLEE: WARNING: killing 11774 states (over memory cap)
KLEE: WARNING: killing 11845 states (over memory cap)
KLEE: WARNING: killing 12077 states (over memory cap)
KLEE: WARNING: killing 11965 states (over memory cap)
KLEE: WARNING: killing 12031 states (over memory cap)
KLEE: WARNING: killing 11739 states (over memory cap)
KLEE: WARNING: killing 11795 states (over memory cap)
