bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---kernel--locking--locktorture.ko_false-unreach-call.cil.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.: 126 429 1610 6934
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_linux_kernel_module_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 0.421925067902
Removed calls to '__const_udelay' (function is undefined)
Defining function torture_random as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '__udelay' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to '__ldv_linux_kernel_locking_spinlock_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'down_write' (function is undefined)
Removed calls to 'up_write' (function is undefined)
Removed calls to 'down_read' (function is undefined)
Removed calls to 'up_read' (function is undefined)
Defining function external_allocated_data as symbolic
Removed calls to '_torture_stop_kthread' (function is undefined)
Removed calls to 'torture_cleanup_end' (function is undefined)
Defining function torture_cleanup_begin as symbolic
Removed calls to 'ldv_after_alloc' (function is undefined)
Defining function torture_onoff_failures as symbolic
Defining function printk as symbolic
Defining function sprintf as symbolic
Removed calls to 'torture_init_end' (function is undefined)
Defining function torture_init_begin as symbolic
Defining function torture_shuffle_init as symbolic
Defining function torture_stutter_init as symbolic
Removed calls to 'set_user_nice' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'stutter_wait' (function is undefined)
Removed calls to 'torture_kthread_stopping' (function is undefined)
Defining function _torture_create_kthread as symbolic
Removed calls to 'torture_shutdown_absorb' (function is undefined)
Defining function schedule_timeout_interruptible as symbolic
Defining function torture_must_stop as symbolic
Defining function schedule_timeout_uninterruptible as symbolic
Defining function __bitmap_weight as symbolic
Removed calls to 'ldv_assert' (function is undefined)
Linked our definitions to these undefined functions:
  strcmp
  strncmp
  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.458348035812
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 159 433 1442 4671
INFO: Starting verification
KLEE: WARNING ONCE: function "lock_torture_writer" has inline asm
KLEE: WARNING ONCE: function "lock_torture_reader" has inline asm
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_9b14bebe-fa5a-4d35-aae3-19f9cff5eb1e/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: flushing 10680 bytes on read, may be slow and/or crash: MO47[10680] allocated at global:
KLEE: ERROR: /tmp/symbiotic-q9w68e/linux-4.0-rc1---kernel--locking--locktorture.ko_false-unreach-call.cil.c:4954: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-q9w68e/linux-4.0-rc1---kernel--locking--locktorture.ko_false-unreach-call.cil.c:4955: memory error: out of bound pointer
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: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_9b14bebe-fa5a-4d35-aae3-19f9cff5eb1e/symbiotic/lib/verifier/__VERIFIER_error.c:9: ASSERTION FAIL: verifier assertion failed
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: unable to write output test case, losing it
Error found.
RESULT: false(unreach-call)

 --- Error trace ---

Error: ASSERTION FAIL: verifier assertion failed
File: /tmp/vcloud-vcloud-master/worker/working_dir_9b14bebe-fa5a-4d35-aae3-19f9cff5eb1e/symbiotic/lib/verifier/__VERIFIER_error.c
Line: 9
assembly.ll line: 563
Stack: 
	#000000563 in __VERIFIER_error () at /tmp/vcloud-vcloud-master/worker/working_dir_9b14bebe-fa5a-4d35-aae3-19f9cff5eb1e/symbiotic/lib/verifier/__VERIFIER_error.c:9
	#100002874 in ldv_struct_noname_2_dummy_resourceless_instance_0 (=0) at /tmp/symbiotic-q9w68e/linux-4.0-rc1---kernel--locking--locktorture.ko_false-unreach-call.cil.c:10183
	#200002795 in ldv_dispatch_register_dummy_resourceless_instance_1_6_5 () at /tmp/symbiotic-q9w68e/linux-4.0-rc1---kernel--locking--locktorture.ko_false-unreach-call.cil.c:5294
	#300003724 in ldv_entry_EMGentry_6 (=0) at /tmp/symbiotic-q9w68e/linux-4.0-rc1---kernel--locking--locktorture.ko_false-unreach-call.cil.c:5750
	#400004524 in main () at /tmp/symbiotic-q9w68e/linux-4.0-rc1---kernel--locking--locktorture.ko_false-unreach-call.cil.c:5773

 --- ----------- ---
Generating witness: /tmp/vcloud-vcloud-master/worker/working_dir_9b14bebe-fa5a-4d35-aae3-19f9cff5eb1e/symbiotic/witness.graphml
Traceback (most recent call last):
  File "bin/symbiotic", line 750, in <module>
    opts.is32bit, False, opts.witness_output)
  File "bin/symbiotic", line 289, in generate_counterexample
    generate_graphml(pth, sources[0], prps, is32bit, is_correctness_wit, saveto)
  File "bin/symbiotic", line 273, in generate_graphml
    gen.parseError(path, source)
  File "/tmp/vcloud-vcloud-master/worker/working_dir_9b14bebe-fa5a-4d35-aae3-19f9cff5eb1e/symbiotic/lib/symbioticpy/symbiotic/witnesses/witnesses.py", line 344, in parseError
    last_id = self._dumpObjects('{0}ktest'.format(pathFile[:-4]), filename)
  File "/tmp/vcloud-vcloud-master/worker/working_dir_9b14bebe-fa5a-4d35-aae3-19f9cff5eb1e/symbiotic/lib/symbioticpy/symbiotic/witnesses/witnesses.py", line 182, in _dumpObjects
    objects = self._parseKtest(ktestfile)
  File "/tmp/vcloud-vcloud-master/worker/working_dir_9b14bebe-fa5a-4d35-aae3-19f9cff5eb1e/symbiotic/lib/symbioticpy/symbiotic/witnesses/witnesses.py", line 155, in _parseKtest
    size, = unpack('>i', f.read(4))
struct.error: unpack requires a string argument of length 4
