You're probably looking for klee_assume. See http://klee.llvm.org/Tutorial-2.html for details.
Paul On 21 Nov 2011, at 07:20, Peng Li wrote: > Hi There > > I have a question about the array access check evaluation. > > Suppose the expression is represented in the following format: 0 <= > 4*idx < 253, if this expression is fed into the solver, > then the solver would evaluate this expression into the result: unknown. > > However, give a precondition: 0<= idx < 64, then the above expression > will be evaluated into a definite answer: true, right? > > Here, I am wondering how to encode a precondition to a symbolic variable > in KLEE, and the expression can be consequently evaluated > based upon that precondition. > > Thanks > > Peng > _______________________________________________ > klee-dev mailing list > [email protected] > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
_______________________________________________ klee-dev mailing list [email protected] http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
