Error in use of polyId in the 1.10 grammar
ID0002212: This issue was created automatically from Mantis Issue 2212. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002212 | Frama-C | Documentation > ACSL | public | 2016-02-25 | 2016-07-22 |
| Reporter | dcok@grammatech.com | Assigned To | patrick | Resolution | won't fix |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Magnesium | Target Version | - | Fixed in Version | - |
Description :
The 1.10 ACSL grammar defines a poly-id as a combination of a simple id, optional label-binders and optional type-var-binders. This is correct for the many places that a poly-id is used as part of a declaration. However, poly-id is also used as a term - either as a standalone variable or as the function name in a function application. Here it is a use of the identifier, so the contents of the type list are type expressions (as in Fig. 2.12), not type variable binders. Similarly the labels are instances of labels (including label literals such as Here), and not binders. (The comment about binders also applies to the predicate application production in Fig. 2.2). Something like a poly-id-use is needed:
poly-id-use ::= id ( { label-use ( , label-use )* } )? ( < type-expr (, type-expr )* > )?
where label-use ::= id | label-literal
label-literal ::= Here | Pre | ...