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.
|ID0002009||Frama-Clang||Documentation > ACSL||public||2014-12-01||2015-02-16|
|Product Version||-||Target Version||-||Fixed in Version||-|
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.