>>> 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 More specifically, the variable "x" in klee_int is actually allocated with malloc under klee vm instead of automatic memory allocation like standard machine. see Executor::executeAlloc-> MemoryManager::allocate call chain. I am also thinking if we can assume klee_int can always give you different addresses, what if two malloc give you the same address if there are some free between them. please correct me if I am wrong
On Thu, Aug 14, 2014 at 10:08 AM, Daniel Liew <[email protected]> wrote: > 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
