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
