[klee-dev] what the third argument in SpecialFunctionHandler::handleMakeSymbolic

[Sumit Kumar]

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 <dan at su-root.co.uk> wrote:

> On 19 March 2016 at 10:23, Sumit Kumar <sumit686215 at 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``.
>
-------------- next part --------------
HTML attachment scrubbed and removed