Hi, I was going through the documentation of KQuery, and I got a little confused about Query Commands.
The documentation says that query-expression is the expression to determine the validity of the query. Does it mean that Klee evaluates query-expression under the constraints defined in costraint-list to see if it is satisfiable? If so, why the query below is invalid? From my understanding, the constraints were saying that (a != 0), and the query expression was saying that if it is possible that (a >= 0). In this case, should (a > 0) be the answer? array a[4] : w32 -> w8 = symbolic (query [(Eq false (Eq 0 N0:(ReadLSB w32 0 a)))] (Eq false (Slt N0 0)) [] [a]) And when I read the documentation, the examples given always have query-expression assigned with false. What does it mean in the context of the query? The last question (sry, I have lots of questions lol) I have is the usage of eval-expr-list. The documentation says, 'If a counterexample is desired for invalid queries, this is a list of expressions for which a possible value should be constructed.' Does it mean that klee only generate examples for invalid queries and how klee uses eval-expr-list to generate test cases? Examples would be much appreciated! Best, Ming
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
