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!_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
