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.
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. Thanks, Mark On Thu, Aug 14, 2014 at 2:18 AM, Chaoqiang Zhang <[email protected]> wrote: > klee will reset the memory object name if you are using the same > variable(the same memory address), see function > SpecialFunctionHandler::handleMakeSymbolic, > So, in this case, your second name overwrite the first one. But the good > thing is that klee also has ObjectState::Array member hold another name, so > if you change the line 1) below inside Executor::getSymbolicSolution into > 2). It can output the correct name. But, I am not sure if this is the right > solution. > > 1) res.push_back(std::make_pair(state.symbolics[i].first->name, values[i])); > > ====>>>>> > > 2) res.push_back(std::make_pair(objects[i]->name, values[i])); > > > > > On Wed, Aug 13, 2014 at 1:41 PM, Mark R. Tuttle <[email protected]> > wrote: > >> Is this a bug in how klee_make_symbolic(adr,size,name) handles the name >> string? >> >> I want to modify ktest-tool so complex data structures are easier to >> read. I want an array of integers to print in a way that looks like an >> array of integers. This leads me to experiment with automating >> construction of names like "x[0]" and "x[1]" for klee_make_symbolic to >> insert into the *.ktest files. >> >> Consider the following code demo.c >> >> #include <klee/klee.h> >> >> int main(int argc, char* argv[]) { >> int array[2]; >> >> #if BLOCK==1 >> array[0] = klee_int("x[0]"); >> array[1] = klee_int("x[1]"); >> #endif >> >> #if BLOCK==2 >> int x; >> klee_make_symbolic(&x,sizeof(x),"x[0]"); >> array[0] = x; >> klee_make_symbolic(&x,sizeof(x),"x[1]"); >> array[1] = x; >> #endif >> >> #if BLOCK==3 >> int x0; >> klee_make_symbolic(&x0,sizeof(x0),"x[0]"); >> array[0] = x0; >> int x1; >> klee_make_symbolic(&x1,sizeof(x1),"x[1]"); >> array[1] = x1; >> #endif >> >> return 0; >> } >> >> Block 1 feels like natural code for inserting symbolic integers into an >> array. Block 2 feels like a natural in-lining of the klee_int function >> that allocates x on the stack, calls klee_make_symbolic, and returns x. >> Block 3 is block 2 without the reuse of x (simulating the result of x on >> the stack). >> >> So I expect them all to use "x[0]" and "x[1]" as the names for array[0] >> and array[1], but that's not what I get running the latest KLEE with >> LLVM/CLANG 3.3: >> >> Block 1 >> >> $LLVM/bin/clang -DBLOCK=1 -c -emit-llvm -I $KLEE/include -o demo.bc demo.c >> $KLEE/bin/klee demo.bc >> $KLEE/bin/ktest-tool klee-last/*.ktest | grep name >> >> object 0: name: 'x[0]' >> object 1: name: 'x[1]' >> >> Block 2 >> >> $LLVM/bin/clang -DBLOCK=2 -c -emit-llvm -I $KLEE/include -o demo.bc demo.c >> $KLEE/bin/klee demo.bc >> $KLEE/bin/ktest-tool klee-last/*.ktest | grep name >> >> object 0: name: 'x[1]' >> object 1: name: 'x[1]' >> >> Block 3 >> >> $LLVM/bin/clang -DBLOCK=3 -c -emit-llvm -I $KLEE/include -o demo.bc demo.c >> $KLEE/bin/klee demo.bc >> $KLEE/bin/ktest-tool klee-last/*.ktest | grep name >> >> object 0: name: 'x[0]' >> object 1: name: 'x[1]' >> >> Is this a bug or am I just doing something stupid? >> >> Thanks, >> Mark >> >> >> >> _______________________________________________ >> klee-dev mailing list >> [email protected] >> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev >> >> >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
