Hi Jonathan,
I only skimmed through your message, but may I first ask why you need to
build another parser for the KQuery language? We already have one, part
of the Kleaver tool. Couldn't you use/extend it in your work?
Best wishes,
Cristian
On 11/04/13 14:12, Jonathan Koch wrote:
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
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
