Hello everyone,
Thank you for the replies!
Cristian, I used upstream STP (I think it was commit ce5f484 at that
time). Stack size and open file limits were definitely set appropriately.
Daniel, the division by zero errors I got could be due to issue #106.
Hristina's suggestion of setting the division_by_zero_returns_one_flag
would be an easy workaround to try. I've currently torn down my
KLEE+Coreutils test environment, but later on I'll set it up again and
test it.
Besides the div zero issue, I also saw this other error: virtual bool
CexCachingSolver::computeValue(const klee::Query&,
klee::ref<klee::Expr>&): Assertion `a && "computeValue() must have
assignment"' failed.
(...)
KLEE: watchdog exiting (no child)
Best regards,
Emil
On 10/8/2014 8:39 PM, Hristina Palikareva wrote:
Hi all,
There is functionality in STP to make division by 0 total and I have
used it to avoid crashes. The code is in make_division_total() -- it
defines x / 0 = 1 and x % 0 = x.
Best regards,
Hristina
On 8 October 2014 11:02, Cadar, Cristian <[email protected]> wrote:
Hi Emil,
What version of STP did you use for these experiments?
If r940, I would try a more recent version of STP. In fact, we would
like to start recommending a more recent version, but we'd like to have
more experience with this first.
The usual cause of this problem is the stack size, but you say you've
already double-checked that. To debug this further, I would suggest to
log the STP queries, reproduce the problem outside KLEE and then report
it to the STP developers.
Just to note there is a known issue with division by zero in STP
https://github.com/stp/stp/issues/106
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
.
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
