nonterminal "predicate" used, but apparently not defined in ACSL grammar
ID0002009: This issue was created automatically from Mantis Issue 2009. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002009 | Frama-Clang | Documentation > ACSL | public | 2014-12-01 | 2015-02-16 |
| Reporter | Jochen | Assigned To | virgile | Resolution | fixed |
| Priority | normal | Severity | feature | Reproducibility | always |
| Platform | frama-c-Neon-20140301+dev-stance | OS | - | OS Version | xubuntu-cfe13.10 |
| Product Version | - | Target Version | - | Fixed in Version | - |
Description :
In the manual "acsl-implementation-Neon-20140301.pdf", the nonterminal "predicate" is used e.g. on the right-hand side of "ensures-clause" (Fig.2.5, p.28). However, manually (see issue #2008 (closed)) scanning though the document, I couldn't find a rule for "predicate".
There is a rule for "pred" in Fig.2.2, p.17, and I guess some rule like "predicate ::= pred | label : predicate" should give the connection between these nonterminals, but I failed to find it.
The index refers to p.16, which in turn refers to Fig.2.1 to 2.3, but none of them contains a definition rule.