On 14 August 2014 16:08, Mark R. Tuttle <[email protected]> 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. _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
