2020-12-05 00:59 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002200Frama-CDocumentation > ACSLpublic2020-02-17 18:08
ReporterJochen 
Assigned Topatrick 
PrioritynormalSeveritytextReproducibilityN/A
StatusclosedResolutionfixed 
PlatformSodium-20150201OSOS Versionxubuntu14.04
Product VersionFrama-C Sodium 
Target VersionFixed in VersionFrama-C 20-Calcium 
Summary0002200: explicitly mention operator precedences when referring to Fig.2.1 "Grammar of terms" in the acsl-implementation manual
DescriptionRunning "frama-c xac2.c" on the attached program results in an error message:
xac.c:20:[kernel] user error: unexpected token ':'
The message disappears if the named subterm "A:1" is put in parantheses.

However, from Fig.2.1 "Grammar of terms" (p.16) in the manual "acsl-implementation-Sodium-20150201.pdf" the derivation
term -----> unary-op term -----> unary-op id : term -----> - A : 1
seems to be perfectly valid.

I suggest that, when referring to Fig.2.1, a note should be added that the grammar should be taken cum grano salis rather than literally, and that operator precedences (probably those shown in Fig.2.4, p.19) apply that aren't reflected in Fig.2.1. A similar note could be added for Fig.2.2 "Grammar of predicates", and maybe also at later places in the manual.
TagsNo tags attached.
Attached Files
  • c file icon xac2.c (54 bytes) 2016-01-04 14:30 -
    //@ ensures \result == - A:1;
    extern int foo(void);
    
    
    c file icon xac2.c (54 bytes) 2016-01-04 14:30 +

-Relationships
+Relationships

-Notes

~0006243

patrick (developer)

Yes, your derivation rule seems perfectly valid.

~0006417

patrick (developer)

As the can see from the first grammar figure (2.1), the grammar is not purely in Backus-Naur Form as written in section 1.3.
Yes, without any precedence rules, the figure does says how to parse the term : "P && Q || R".
That is the purpose of the section 2.2.1
That section explains the "-A:1" shoud be parsed as "(-A):1" that is not an ACSL term.
 
May be, something can be added into section 1.3

~0006823

patrick (developer)

There is such a rule in Figure 2.1 & 2.2 about "syntactic naming" and precedence is given in Figure 2.4 of the document version: acsl-implementation-19.0-Potassium.pdf

Note: next issues about ACSL has to be reported at https://github.com/acsl-language/acsl/issues

~0006938

signoles (manager)

Fixed in Frama-C 20.0 (Calcium).
+Notes

-Issue History
Date Modified Username Field Change
2016-01-04 14:30 Jochen New Issue
2016-01-04 14:30 Jochen Status new => assigned
2016-01-04 14:30 Jochen Assigned To => signoles
2016-01-04 14:30 Jochen File Added: xac2.c
2016-01-04 14:34 signoles Assigned To signoles => maroneze
2016-06-21 14:11 signoles Category Documentation => Documentation > ACSL
2016-06-21 14:26 signoles Assigned To maroneze => patrick
2016-07-22 09:59 patrick Status assigned => acknowledged
2016-07-22 10:05 patrick Note Added: 0006243
2017-06-28 10:30 patrick Note Added: 0006417
2019-07-17 11:09 patrick Note Added: 0006823
2019-07-17 11:09 patrick Status acknowledged => resolved
2019-07-17 11:09 patrick Fixed in Version => Frama-C 19-Potassium
2019-07-17 11:09 patrick Resolution open => fixed
2020-02-17 18:06 signoles Fixed in Version Frama-C 19-Potassium => Frama-C 20-Calcium
2020-02-17 18:08 signoles Status resolved => closed
2020-02-17 18:08 signoles Note Added: 0006938
+Issue History