[klee-dev] how to know if variable is symbolic

[Andrew Santosa]

Hi Sumit,
Presumably you are looking into Executor::executeInstruction method.If you take a look at, for example the code that handle LLVM'sInstruction::Add right after "case Instruction::Add:"
     ref<Expr> left = eval(ki, 0, state).value;
    ref<Expr> right = eval(ki, 1, state).value;
    ref<Expr> result = AddExpr::create(left, right);
    bindLocal(ki, state, result);
You can check whether left is a constant or not using
llvm::isa<ConstantExpr>(left.get())

In case the above returns false, then left is some expressioninvolving symbolic variables, which you can examine by executing
left->dump();
Similarly with right. I hope this answers your question.

Best,
Andrew
 

    On Friday, 18 March 2016, 1:18, Sumit Kumar <sumit686215 at gmail.com> wrote:
 

 Hi,
I want to know if there is a way to know if a variable is symbolic or not in KLEE when KLEE is executing an instruction involving the variable.

--
Thanks and Regards,
Sumit

_______________________________________________
klee-dev mailing list
klee-dev at imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev


  
-------------- next part --------------
HTML attachment scrubbed and removed