search

acsl-language / acsl

Sources for the ANSI/ISO C Specification Language manual
Other
47 stars 8 forks source link

Grammar adjustments to correct and distinguish between type names and type expressions, and to be explicit about C type grammar #62

Closed davidcok closed 4 years ago

davidcok commented 4 years ago

In C declarations, the (and any [] ) are part of the variable-ident, as is the case in the binder grammar. So the original grammar was ambiguous, as the could be part of the type-expr or the variable-ident

There are situations in which a type-expr with * etc. and without a variable name are needed, such as in cast expressions. C grammar calls these abstract declarators.

However, the grammar for a parameter is type-expr id, which permits (and requires) the non-C declaration style int[] a .

So unless the intention is to encourage the non-C styule of declaration, the grammar for parameter needs to change as well. I'm going to be reviewing all of these declaration grammar elements this weekend (in Brittany I hope). Your comments today would be welcome.

On Tue, Jul 23, 2019 at 5:19 PM Virgile Prevosto notifications@github.com wrote:

@vprevosto requested changes on this pull request.

See question about binder grammar rule.

In binders.tex https://github.com/acsl-language/acsl/pull/62#discussion_r306380453:

@@ -1,12 +1,14 @@ \begin{syntax} binders ::= binder (, binder)* ; \

  • binder ::= type-expr variable-ident;
  • binder ::= type-name variable-ident;

I don't understand this change. As far as I can tell, this would prevent writing something like assert list_positive: \forall list p; reachable(root, p) ==> p->content > 0; unless we have an explicit typedef for list .

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHub https://github.com/acsl-language/acsl/pull/62?email_source=notifications&email_token=ABITDQEDSSXOW6OQZVRW2ZTQA4ORVA5CNFSM4H4NADR2YY3PNVWWK3TUL52HS4DFWFIHK3DMKJSXC5LFON2FEZLWNFSXPKTDN5WW2ZLOORPWSZGOB7JP2FA#pullrequestreview-265485588, or mute the thread https://github.com/notifications/unsubscribe-auth/ABITDQEXQ7ERALBSXMIQN3LQA4ORVANCNFSM4H4NADRQ .