acsl-language / acsl

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

shadowing behavior ids #35

Open davidcok opened 6 years ago

davidcok commented 6 years ago

statement contracts can be nested in other statement or function contracts. So nested behaviors may have the same ids. We can forbid this or we can declare the inner ids shadow the outer; the text is written as the latter at the moment. Anyone object?

vprevosto commented 6 years ago

@jensgerlach @backtracking @pbaudin for comments

pbaudin commented 6 years ago

the inner ids shadow the outer is OK for me. That is consistent with the text in section 2.4.1 about the use of for bhv-id : a-clause ;.

jensgerlach commented 6 years ago

I wonder whether a tool that processes nested statement contracts should be required to report shadowing.

davidcok commented 6 years ago

An alternative to shadowing semantics is to forbid reusing names - so tools would then be required to report name conflicts. Do you prefer forbidding or shadowing or something in between (e.g. shadowing with a mandatory warning)?

On Mar 9, 2018, at 3:16 PM, Jens Gerlach notifications@github.com wrote:

I wonder whether a tool that processes nested statement contracts should be required to report shadowing.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/acsl-language/acsl/issues/35#issuecomment-371823935, or mute the thread https://github.com/notifications/unsubscribe-auth/AFExwBhmqspWzRjJGQO_eG-MIsrwisKfks5tco7RgaJpZM4Si4AL.