[klee-dev] kquery: versions. version-specifier and version labels

[Jonathan Koch]

Hallo everybody,

I am building a parser to reconstruct the AST for KQuery expressions.
However, I ran into 3 points in the language definition that are not
quite clear to me.

In the section "Expression and Version Labels" it says "Likewise,
versions are frequently shared among reads and can be labelled in the
same fashion." What does this mean exactly?
Does it mean
    version = identifier ":" version
or does it mean
    expression = identifier ":" version

In the definition of "Read", "ReadLSB" and "ReadMSB" a terminal-symbol
"version-specifier" is used. At this point it is really not clear to me
what is meant by this.
At first I thought it is just an identifier/version but this contradicts
"(Read w8 mem 0)" (given as an example in the "Query Commands"-Section).
0 can only be a numeric-literal, how does this fit into the definition?

On the KQuery reference page "version" is never used explicitly on any
RHS of a syntax-rule. Maybe this is already covered by the questions
above or maybe I just missed something.

Besides that I found one minor mistake:
In the syntax-definition of array the following is stated:
    array-initializer = "symbolic" | "[" { numeric-literal } "]"
This does not match the example given in the same section (commas
missing in the definition?)
    array foo[] : w8 -> w1 = [ true, false, false, true ]

I would highly appreciate some help. Other than that: I really love
KLEE, it is a truly amazing tool you built.

Best regards,
Jonathan