[klee-dev] Questions about KQuery language

[箜]

Hello.
        These days I am reading the source code about constraint solver in klee. I have some questions about the KQuery language and the sovler's implementation.

1) Does the KQuery language has any detail documents or some API that I can use to going on my own implementation. Does the language only used by the klee, that was invented by klee developer?

2) What is the difference between expression label and version label? Does the difference is expression label just like variable in the source code level while version label must have the write operation to change the array's element?

3) What is the meaning of the domain and range in the definition of array? In the file Expr.h, the comment said "Domain is how many bits can be used to access the array", does this means that I access the array element by the way in 4 bytes alignment, I access 4 bytes, 32 bits once operation to array. "Range is the size (in bits) of the number stored there", this means that each element in the array is "range" bits? I am not understand these statement, do you give me some example to help me figure it out?

4) The document of the KQuery language states the "floating-point-type = "fp[0-9]+([.].*)?" " integer-type = "i[0-9]+"" are reserved keywords and supports 2 kinds of declarations, if I want the KQuery language supports the declaration of float point type and int type, what should I do? Do I need implement a class FloatPoint and Int in the file Expr.h?

5) In the language, SExt ZExt these are all states that evaluates to the lower type bits of child-expression, what is the lowest type bits, could you give me any example to figure it out? I am confused with the lowest type bits.
    Thanks you very much!
-------------- next part --------------
HTML attachment scrubbed and removed