[klee-dev] Coreutils: STP division by zero errors and computeValue assertion failures

[Emil Rakadjiev]

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 <c.cadar at imperial.ac.uk> 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
>> klee-dev at imperial.ac.uk
>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
> .
>