search

acsl-language / acsl

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

Slight changes to allow mixing kinds of global declarations in one comment #61

Closed davidcok closed 4 years ago

davidcok commented 5 years ago

…ation comment

davidcok commented 5 years ago

OK - that works. It implies also that a data-inv-decl can be in an axiomatic, which to me is OK as well.

On Jul 11, 2019, at 6:21 PM, Virgile Prevosto notifications@github.com wrote:

@vprevosto commented on this pull request.

In data_invariants.tex https://github.com/acsl-language/acsl/pull/61#discussion_r302632769:

@@ -1,5 +1,5 @@ \begin{syntax}

  • declaration ::= "/@" data-inv-decl "/"
  • acsl-annot ::= data-inv-decl I agree with @pbaudin https://github.com/pbaudin data-inv-def could simply be part of logic-def, there's no need to make a special case for it at this point.

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