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
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
