explicitly mention operator precedences when referring to Fig.2.1 "Grammar of terms" in the acsl-implementation manual
ID0002200: This issue was created automatically from Mantis Issue 2200. Further discussion may take place here.
|ID0002200||Frama-C||Documentation > ACSL||public||2016-01-04||2020-02-17|
|Product Version||Frama-C Sodium||Target Version||-||Fixed in Version||Frama-C 20-Calcium|
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.