symbolic values and expression

[Bo Fang]

Hi all,

I am new to Klee and maybe I am just asking a naive question. What I am
doing here is that I try to convert an instruction to an "error" state,
meaning that using a "not equal" expression as a constraint for the
original expression. So here is a example of code:

Inside the Executor::executeInstruction(), I add this in one of the
switch-case segments. In this example I show the Add case:

unsigned size =
kmodule->targetData->getTypeAllocSize(ki->inst->getType());
klee_make_symbolic(ki->inst,size,ki->inst->getOpcodeName());
ref<Expr> ret = NeExpr::create(ki->inst,AddExpr::create(left,right));
addConstraint(state,ret);

The line highlighted was that I don't know how to solve. Could someone help
me validate the idea or point out how to do this? Thanks!

Bo