2014-09-26 01:51:10 UTC
I repeated the Coreutils experiment using the information from the
website (very useful, thank you!), and I noticed that for some
applications, the KLEE execution fails and exits prematurely with one of
the following two errors (some more details can be found in the attached
klee: /home/er/klee/klee/lib/Solver/CexCachingSolver.cpp:311: virtual
bool CexCachingSolver::computeValue(const klee::Query&,
klee::ref<klee::Expr>&): Assertion `a && "computeValue() must have
KLEE: watchdog exiting (no child)
Fatal Error: BVConstEvaluator:division by zero error
error: STP Error: BVConstEvaluator:division by zero error
ERROR: STP did not return successfully. Most likely you forgot to run
'ulimit -s unlimited'
My configuration: Ubuntu 14.04, LLVM 2.9, KLEE upstream, STP upstream,
Coreutils 6.10, set up exactly as described on the website, KLEE
arguments also from the website with one change: --max-time=1800.
(instead of 3600).
My stack size limit was set to unlimited (and I also had to raise the
open file limit, because I got KLEE errors with the default system limits).
I ran all the 89 applications, on two separate, identically configured
machines simultaneously. Results:
PC1: cp, ginstall; PC2: ginstall
PC1: ls, pr, stat, tsort; PC2: stat, tsort
Then, I reran only the failed symbolic executions, and some of them
completed successfully. Results:
PC1: cp; PC2: ginstall
PC1: pr, stat, tsort; PC2: tsort
And, for the third time, I ran again the few failing applications from
run 2 with KLEE:
PC1: (none); PC2: ginstall
PC1: stat, tsort; PC2: tsort
Do you know what the reason for those sporadic failures could be?
As mentioned above, I attached two files containing the detailed error
messages (incl. some preceding output) from the first run. If you need
further details, please let me know.