Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002143Frama-CDocumentation > ACSLpublic2015-07-06 20:532016-01-26 08:52
Reportergaggarwal 
Assigned Topatrick 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
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

-  Notes
(0006023)
patrick (developer)
2015-09-07 11:26

Grammar of function application/predicate application has been corrected.

- 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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker