ID0002143: **This issue was created automatically from Mantis Issue 2143. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0002143 | Frama-C | Documentation > ACSL | public | 2015-07-06 | 2016-01-26 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | gaggarwal | **Assigned To** | patrick | **Resolution** | fixed | | **Priority** | normal | **Severity** | minor | **Reproducibility** | always | | **Platform** | - | **OS** | - | **OS Version** | - | | **Product Version** | Frama-C Sodium | **Target Version** | Frama-C Magnesium | **Fixed in Version** | Frama-C Magnesium | ### Description : Following is the grammar of Function Application in acsl-1.9.pdf in Fig 2.1: term :: = id (term (, term)*) and grammar of predicate application is : pred ::= id (term (, term)*) But a function application/predicate application can include label-binders like: For function definition : logic integer max{L}(integer n1, integer n2 ) = (n1 <=n2)? n2 : n1; we can call this function as: ensures max{L}(n1, n2); Grammar of function application/predicate application should include label-binders.