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

[Emil Rakadjiev]

Hristina, I tried your suggestion today and added a 
make_division_total(vc); call to the STPSolverImpl constructor in 
lib/Solver/Solver.cpp (line 557).

I already did 3 (the 4th is running) 30 min runs on the ginstall tool 
and, as expected, I haven't seen the div zero error so far. I want to do 
further tests, because they are not deterministic in this regard. I also 
want to test if this has any effect on the other error I encountered.

What side-effects does this workaround have on KLEE (if any)?
Thank you!

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
>
> .
>