hello, KLEE translate the llvm bytecode into expressions along forward execution. So when I translate the instructions backward along a trace, I think I should firstly create a dummy expression which will by updated by some instruction before the current instruction.
Take the next bytecode for example: 30 %10 = load i32* %x1, align 4, !dbg !17 dummyExpr%10 = Exprx1 (update dummyExpr%10) ---- third step ↑ 31 %11 = load i32* %x2, align 4, !dbg !17 dummyExpr%11 = Exprx2 (update dummyExpr%11) ---- second step ↑ 32 %12 = icmp slt i32 %10, %11, !dbg !17 Expr12 = (slt dummyExpr%10, dummyExpr%11) ---- fisrt step ↑ But I didn't find a proper API to create a dummy expression, who can tell me? OR somebody know some other clever method for executing backward? Thank you very much. -------------------------------------------- Qiuping Yi Institute Of Software Chinese Academy of Sciences
_______________________________________________ klee-dev mailing list [email protected] http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
