[klee-dev] Understanding of KQuery

[Yao, Mingxuan]

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
-------------- next part --------------
HTML attachment scrubbed and removed