[klee-dev] bug in klee/stp

[Marek Chalupa]

Hi,

On 02/02/16 12:08, Sven wrote:
> hi,
>
> You have integer arithmetics here (this is C, after all). This code:
>
> int main(void) {
>          int n = -1;
>          int d = n/2;
>          printf("Result: %d\n", d);
> }
>
> prints 0. The problem is that 1/2 is not an integer number, so it is
> rounded down. In integer arithmetics 1/2 == 0. The same goes for -1.
>
> So the assumption holds, because n == -1 < 0. But also n/2 == -1/2 == 0,
> so the body of the if statement (and thereby the assertion) is executed.

if n/2 == -1/2 == 0 then condition (n/2 > 0) --> (0 > 0) is false, isn't 
it? So the assert should not be called for n == -1

If I use:

klee_assume(n < 0)
klee_assume(n > -10)

then klee hits the assert and ktest-tool says that n == -9 on that path.
When I use:

klee_assume(n == -9)

no assertion is hit. That does not look like correct to me... or I just 
still don't get what's happening here

Thanks,
Marek

>
> This is not a bug in klee, but just how integer arithmetics work.
>
> Alex
>
> PS: I would not even attribute this to the SMT solver, both gcc and
> clang generate code which handles it the same way, so klee is absolutely
> correct here.
>
> On 02/02/2016 10:06 AM, Marek Chalupa wrote:
>> Hi list,
>>
>> I have this small trivial program:
>>
>>
>> #include <assert.h>
>>
>> int main(void)
>> {
>>    int n;
>>    klee_make_symbolic(&n, sizeof n, "n");
>>    klee_assume(n < 0);
>>
>>    if (n/2 > 0)
>>      assert(0);
>>
>>    return 0;
>> }
>>
>>
>> KLEE (on master from git) says that the assertion is violated,
>> although since n is negative, then n/2 should not be greater than 0
>> and the assert() should be never called. I suppose it is a bug, or did
>> I overlook something?
>>
>> P.S. If the condition is just (n > 0), then everything is fine. The
>> assumption can be even (n < -1) or (n < -1 && n > -10) (in which case
>> I get that the assumption is provably false, which is weird also)
>>
>> Thanks,
>> Marek
>>
>> _______________________________________________
>> 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
>