\myheading{strtodx() from RetroBSD} Just found this function in RetroBSD: \url{https://github.com/RetroBSD/retrobsd/blob/master/src/libc/stdlib/strtod.c}. It converts a string into floating point number for given radix. \lstinputlisting[numbers=left]{KLEE/strtodx.c} ( \url{\RepoURL/\CURPATH/strtodx.c} ) Interestingly, KLEE cannot handle floating-point arithmetic, but nevertheless, found something \footnote{All timings are when KLEE 3.0 running on AMD Ryzen 5 3600.}: \begin{lstlisting} % clang -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -I /tmp/klee_src/include/klee/ strtodx.c % time klee --libc=uclibc --optimize strtodx.bc ... KLEE: ERROR: strtodx.c:204: memory error: out of bound pointer KLEE: NOTE: now ignoring this error at this location KLEE: done: total instructions = 303616 KLEE: done: completed paths = 2150 KLEE: done: partially completed paths = 1904 KLEE: done: generated tests = 2151 real 3m23.710s user 2m48.737s ... % ls klee-last | grep err test000155.ptr.err % ktest-tool klee-last/test000155.ktest | grep data object 0: data: b'.0f-79\x00' \end{lstlisting} As it seems, the ``.0f-79'' string does out of bounds array access (read) at the line 204. During further investigation, I've found that \TT{powersOf10[]} array is too short: 6th element (started at 0th) has been accessed. And here we see a part of array commented (line 81)! Probably someone's mistake? Unfixed bug?