Frama-C Bug Tracking System - Frama-C
View Issue Details
0002143Frama-CDocumentation > ACSLpublic2015-07-06 20:532016-01-26 08:52
gaggarwal 
patrick 
normalminoralways
closedfixed 
Frama-C Sodium 
Frama-C MagnesiumFrama-C Magnesium 
0002143: Incorrect grammar of Predicate Application and Function Application
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.
No tags attached.
Issue History
2015-07-06 20:53gaggarwalNew Issue
2015-07-06 20:53gaggarwalStatusnew => assigned
2015-07-06 20:53gaggarwalAssigned To => signoles
2015-07-07 08:52signolesAssigned Tosignoles => maroneze
2015-08-08 09:19signolesTarget Version => Frama-C Magnesium
2015-09-04 10:50bobotAssigned Tomaroneze => patrick
2015-09-07 11:26patrickNote Added: 0006023
2015-09-07 11:26patrickStatusassigned => resolved
2015-09-07 11:26patrickResolutionopen => fixed
2016-01-26 08:51signolesFixed in Version => Frama-C Magnesium
2016-01-26 08:52signolesStatusresolved => closed
2016-06-21 14:11signolesCategoryDocumentation => Documentation > ACSL

Notes
(0006023)
patrick   
2015-09-07 11:26   
Grammar of function application/predicate application has been corrected.