Skip to content

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.


Id Project Category View Due Date Updated
ID0002200 Frama-C Documentation > ACSL public 2016-01-04 2020-02-17
Reporter Jochen Assigned To patrick Resolution fixed
Priority normal Severity text Reproducibility N/A
Platform Sodium-20150201 OS - OS Version xubuntu14.04
Product Version Frama-C Sodium Target Version - Fixed in Version Frama-C 20-Calcium

Description :

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.

Attachments

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information