This appendix presents the complete grammar for the annotation language. We use the following type face conventions: Italic font for non-terminals, bold typewriter font for literal terminals including keywords, and SMALL CAPS for the lexicographic terminals such as identifiers and C code fragments. In addition, we use the square brackets to represent optional components, and the star to represent repetition of a component.