On 04/03/2012 02:08 PM, Don Clugston wrote:
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?
Don't allow forward referencing function a() if there is an intervening
order-dependent declaration.
(Alternatively, just analyse which symbols are referenced where and
don't allow calling a local function that can transitively reach some
symbols that have not yet been declared. I think this might be too
complicated to be justifiable.)
