Nested functions should be exempt from sequential visibility rules

[Don Clugston]

On 03/04/12 13:58, Timon Gehr wrote:
> On 04/03/2012 01:55 PM, Don Clugston wrote:
>> On 03/04/12 13:35, Timon Gehr wrote:
>>> On 04/03/2012 01:08 PM, Don Clugston wrote:
>>>>
>>>> Y b() { ... }
>>>> Y y = b();
>>>> X x = ...
>>>>
>>>> Prove that y doesn't depend on x.
>>>
>>> Since only function declarations are immune to ordering rules, b cannot
>>> forward reference x.
>>
>> But there could be another function a() which is below x, and which b()
>> calls.
>
> This scenario can be forbidden conservatively.

How?