Frama-C Bug Tracking System - Frama-C
View Issue Details
0002200Frama-CDocumentation > ACSLpublic2016-01-04 14:302019-07-17 11:09
Jochen 
patrick 
normaltextN/A
resolvedfixed 
Sodium-20150201xubuntu14.04
Frama-C Sodium 
Frama-C 19-Potassium 
0002200: explicitly mention operator precedences when referring to Fig.2.1 "Grammar of terms" in the acsl-implementation manual
Running "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.
No tags attached.
c xac2.c (54) 2016-01-04 14:30
https://bts.frama-c.com/file_download.php?file_id=1078&type=bug
Issue History
2016-01-04 14:30JochenNew Issue
2016-01-04 14:30JochenStatusnew => assigned
2016-01-04 14:30JochenAssigned To => signoles
2016-01-04 14:30JochenFile Added: xac2.c
2016-01-04 14:34signolesAssigned Tosignoles => maroneze
2016-06-21 14:11signolesCategoryDocumentation => Documentation > ACSL
2016-06-21 14:26signolesAssigned Tomaroneze => patrick
2016-07-22 09:59patrickStatusassigned => acknowledged
2016-07-22 10:05patrickNote Added: 0006243
2017-06-28 10:30patrickNote Added: 0006417
2019-07-17 11:09patrickNote Added: 0006823
2019-07-17 11:09patrickStatusacknowledged => resolved
2019-07-17 11:09patrickFixed in Version => Frama-C 19-Potassium
2019-07-17 11:09patrickResolutionopen => fixed

Notes
(0006243)
patrick   
2016-07-22 10:05   
Yes, your derivation rule seems perfectly valid.
(0006417)
patrick   
2017-06-28 10:30   
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   
2019-07-17 11:09   
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 [^]