2021-03-01 05:15 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002143Frama-CDocumentation > ACSLpublic2016-01-26 08:52
Reportergaggarwal 
Assigned Topatrick 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Sodium 
Target VersionFrama-C MagnesiumFixed in VersionFrama-C Magnesium 
Summary0002143: Incorrect grammar of Predicate Application and Function Application
DescriptionFollowing 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.
TagsNo tags attached.
Attached Files

-Relationships
+Relationships

-Notes

~0006023

patrick (developer)

Grammar of function application/predicate application has been corrected.
+Notes

-Issue History
Date Modified Username Field Change
2015-07-06 20:53 gaggarwal New Issue
2015-07-06 20:53 gaggarwal Status new => assigned
2015-07-06 20:53 gaggarwal Assigned To => signoles
2015-07-07 08:52 signoles Assigned To signoles => maroneze
2015-08-08 09:19 signoles Target Version => Frama-C Magnesium
2015-09-04 10:50 bobot Assigned To maroneze => patrick
2015-09-07 11:26 patrick Note Added: 0006023
2015-09-07 11:26 patrick Status assigned => resolved
2015-09-07 11:26 patrick Resolution open => fixed
2016-01-26 08:51 signoles Fixed in Version => Frama-C Magnesium
2016-01-26 08:52 signoles Status resolved => closed
2016-06-21 14:11 signoles Category Documentation => Documentation > ACSL
+Issue History