Annotation in CFA grammar

[as3810t]

[Feature Request]

The aim of this feature request is to provide annotation capabilities for the CFA grammar. As there are tools (such as GAZER, or the tool requested in #65 ) that emit CFA code, it would be useful to have annotations for different language elements in the CFA, which would make for such tools easier to parse the counterexample, providing traceability.

[as3810t]

Proposed syntax 1

@{ key1 -> val1, key2 -> val2, ... }
process main() {
  @{ key1 -> val1, key2 -> val2, ... }
  var x: int

  @{ key1 -> val1, key2 -> val2, ... }
  loc L1
  loc L2

  @{ key1 -> val1, key2 -> val2, ... }
  L1 -> L2 {
    stmts...
  }
}

[as3810t]

Proposed syntax 2

process main() @{ key1 -> val1, key2 -> val2, ... } {
  var x: int @{ key1 -> val1, key2 -> val2, ... }

  loc L1 @{ key1 -> val1, key2 -> val2, ... }
  loc L2

  L1 -> L2 @{ key1 -> val1, key2 -> val2, ... } {
    stmts...
  }
}

[vincemolnar]

I don't like the -> because it interferes with the transitions. I'd prefer = or :.

[hajduakos]

Boogie has something like this:

var {:key1 value1} {:key2 value2} ... x

But we don't have to stick to this, just an example.