|Anonymous | Login | Signup for a new account||2017-11-20 07:00 CET|
|Main | My View | View Issues | Change Log | Roadmap | Repositories|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0002200||Frama-C||Documentation > ACSL||public||2016-01-04 14:30||2017-06-28 10:30|
|Product Version||Frama-C Sodium|
|Target Version||Fixed in Version|
|Summary||0002200: explicitly mention operator precedences when referring to Fig.2.1 "Grammar of terms" in the acsl-implementation manual|
|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.
|Tags||No tags attached.|
|Attached Files||xac2.c [^] (54 bytes) 2016-01-04 14:30 [Show Content]|
|Yes, your derivation rule seems perfectly valid.|
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
|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|
|Copyright © 2000 - 2017 MantisBT Team|