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

[Cristian Cadar]

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
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>