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

Dan Liew dan at su-root.co.uk
Sat Mar 19 12:36:51 GMT 2016


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``.




More information about the klee-dev mailing list