bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.4-simple/43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--clocksource--cs5535-clockevt.ko-ldv_main0_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.: 13 18 95 596
INFO: Compilation, preparation and instrumentation time: 0.0567998886108
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'cs5535_mfgpt_free_timer' (function is undefined)
Removed calls to 'cs5535_mfgpt_write' (function is undefined)
Removed calls to 'clockevents_register_device' (function is undefined)
Removed calls to 'ldv_check_final_state' (function is undefined)
Defining function cs5535_mfgpt_read as symbolic
Defining function cs5535_mfgpt_alloc_timer as symbolic
Defining function printk as symbolic
Defining function setup_irq as symbolic
Defining function clockevent_delta2ns as symbolic
Defining function cs5535_mfgpt_set_irq as symbolic
Defining function ldv_some_page as symbolic
Defining function kmem_cache_alloc as symbolic
Linked our definitions to these undefined functions:
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 0.0651381015778
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 47 24 60 296
INFO: Starting verification
KLEE: ERROR: /tmp/symbiotic-Q4gP2r/43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--clocksource--cs5535-clockevt.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:493: invalid function pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 16651 states (over memory cap)
KLEE: WARNING: killing 14476 states (over memory cap)
KLEE: WARNING: killing 17178 states (over memory cap)
KLEE: WARNING: killing 14362 states (over memory cap)
KLEE: WARNING: killing 17049 states (over memory cap)
KLEE: WARNING: killing 15645 states (over memory cap)
KLEE: WARNING: killing 14275 states (over memory cap)
KLEE: WARNING: killing 15510 states (over memory cap)
KLEE: WARNING: killing 13996 states (over memory cap)
KLEE: WARNING: killing 13733 states (over memory cap)
KLEE: WARNING: killing 14667 states (over memory cap)
KLEE: WARNING: killing 13371 states (over memory cap)
KLEE: WARNING: killing 13941 states (over memory cap)
KLEE: WARNING: killing 14772 states (over memory cap)
KLEE: WARNING: killing 15063 states (over memory cap)
KLEE: WARNING: killing 14447 states (over memory cap)
KLEE: WARNING: killing 13212 states (over memory cap)
KLEE: WARNING: killing 14662 states (over memory cap)
KLEE: WARNING: killing 12670 states (over memory cap)
KLEE: WARNING: killing 14609 states (over memory cap)
KLEE: WARNING: killing 12653 states (over memory cap)
KLEE: WARNING: killing 12592 states (over memory cap)
KLEE: WARNING: killing 14254 states (over memory cap)
KLEE: WARNING: killing 12319 states (over memory cap)
KLEE: WARNING: killing 14081 states (over memory cap)
KLEE: WARNING: killing 12311 states (over memory cap)
KLEE: WARNING: killing 12728 states (over memory cap)
KLEE: WARNING: killing 12427 states (over memory cap)
KLEE: WARNING: killing 13924 states (over memory cap)
KLEE: WARNING: killing 12536 states (over memory cap)
KLEE: WARNING: killing 12117 states (over memory cap)
KLEE: WARNING: killing 12175 states (over memory cap)
KLEE: WARNING: killing 12825 states (over memory cap)
KLEE: WARNING: killing 12174 states (over memory cap)
KLEE: WARNING: killing 11886 states (over memory cap)
KLEE: WARNING: killing 12408 states (over memory cap)
KLEE: WARNING: killing 11996 states (over memory cap)
KLEE: WARNING: killing 12170 states (over memory cap)
KLEE: WARNING: killing 11772 states (over memory cap)
KLEE: WARNING: killing 11831 states (over memory cap)
