KLEE: NOTE: Using POSIX model: /tmp/klee_build60stp_z3/Debug+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: NOTE: Using libcxx : /tmp/klee_build60stp_z3/Debug+Asserts/lib/libc++.bca
KLEE: NOTE: Using klee-uclibc : /tmp/klee_build60stp_z3/Debug+Asserts/lib/klee-uclibc.bca
KLEE: output directory is "/home/klee/build/klee-out-13"
KLEE: Using STP solver backend
warning: Linking two modules of different target triples: build/testbench_sensor' is 'x86_64-unknown-linux-gnu' whereas '__uClibc_main.os' is 'x86_64-pc-linux-gnu'

KLEE: WARNING: undefined reference to function: _Unwind_DeleteException
KLEE: WARNING: undefined reference to function: _Unwind_GetIP
KLEE: WARNING: undefined reference to function: _Unwind_GetLanguageSpecificData
KLEE: WARNING: undefined reference to function: _Unwind_GetRegionStart
KLEE: WARNING: undefined reference to function: _Unwind_RaiseException
KLEE: WARNING: undefined reference to function: _Unwind_SetGR
KLEE: WARNING: undefined reference to function: _Unwind_SetIP
KLEE: WARNING ONCE: Using zero size array fix for landingpad instruction filter
KLEE: WARNING ONCE: Alignment of memory from call "realloc" is not modelled. Using alignment of 8.
KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 121704960) at /tmp/klee_src/runtime/POSIX/fd.c:980 10
KLEE: WARNING ONCE: calling __user_main with extra arguments.
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: WARNING ONCE: calling __klee_posix_wrapped_main with extra arguments.
KLEE: WARNING ONCE: Alignment of memory from call "_Znwm" is not modelled. Using alignment of 8.
KLEE: ERROR: /home/klee/source/bench_sensor.cpp:29: ASSERTION FAIL: interrupt == tig.triggered_irq
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: Alignment of memory from call "_Znam" is not modelled. Using alignment of 8.
KLEE: ERROR: /home/klee/source/bench/sensor.hpp:45: ASSERTION FAIL: len > 0 && "invalid read with length = 0"
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /home/klee/source/bench/sensor.hpp:55: ASSERTION FAIL: len == 4 && "only allow to read/write whole register"
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /home/klee/source/bench/sensor.hpp:58: ASSERTION FAIL: addr <= offsetof(union Memory, filter) && "access to non-mapped address"
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /home/klee/source/bench/sensor.hpp:50: ASSERTION FAIL: (addr + len) <= sizeof(memory.data_frame) && "read out of memory map"
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /home/klee/source/bench_sensor.cpp:59: ASSERTION FAIL: rand_value < 58
KLEE: NOTE: now ignoring this error at this location

KLEE: done: total instructions = 875297
KLEE: done: completed paths = 70
KLEE: done: generated tests = 6

real	0m3.591s
user	0m3.112s
sys	0m0.476s