[klee-dev] klee_make_symbolic bug?

[Daniel Liew]

On 14 August 2014 16:08, Mark R. Tuttle <markrtuttle at gmail.com> wrote:
> Thanks.  I believe you.
>
> My reason for writing, though, was that Block 1 should also be using the
> same memory address for the two name strings, but it works without suffering
> from the overwrite you describe.

But the string you pass into klee_int() specifies the string name for
that symbolic and that is exactly what you are observing.

> Specifically, there is no use of the stack between the two calls to
> klee_int, so the memory used on the stack should be the same by the two
> invocations to klee_int.  I'm guessing the stack is treated differently.

No. klee_int() is part of KLEE's runtime and can be seen at [1]

calling into klee_int() will cause KLEE to enter the klee_int()
function and a variable on klee_int's stack is used as the address of
the symbolic. Even if klee_int() was inlined this would still work
correctly.

[1] https://github.com/klee/klee/blob/master/runtime/Intrinsic/klee_int.c

You might find it informative to look at the LLVM IR that is actually
being executed (look at klee-last/assembly.ll).

Thanks,
Dan.