Thank you Dan. Its more clear now. There is one more thing I am unable understand. The third argument to the function "klee_make_symbolic()" is a string. Which means that I need to create a ref<Expr> object from a string if I want to add it to the "arguments" vector (to make a call to handleMakeSymbolic). However, Expr class does not provide any method / constructor to create a Expr object directly from a string object. It seems that I must instead create ref<Expr> object from the address of string. So I typecasted the address containted in the pointer to 'c' string (obtained using string::c_str()) and created a ref<ConstantExpr> object out of it. But when add it to arguments vector and call 'handleMakeSymbolic' method the assertion in "readStringAtAddress" method fails: Assertion `0 && "XXX out of bounds / multiple resolution unhandled"' failed. Can you tell me what is going wrong here.
-- Thanks and Regards Sumit On 19 March 2016 at 18:06, Dan Liew <d...@su-root.co.uk> wrote: > On 19 March 2016 at 10:23, Sumit Kumar <sumit686...@gmail.com> wrote: > > Hi, > > > > Can anyone please explain what the third argument is in the following > > function/method: > > > > SpecialFunctionHandler::handleMakeSymbolic(ExecutionState &state, > > KInstruction *target, std::vector<ref<Expr> > &arguments) > > > > Please explain what expressions are supposed to be contained in > "arguments" > > vector. Its not clear from the code. > > In this case they are the arguments to the function > ``klee_make_symbolic()`` with argument 0 being the left most argument. > Each argument will be the expression that represents that argument. If > the arguments are a constant they will be of type ``ConstantExpr``. >
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
