> We may repeatedly > walk over a function body because it is successively contified in > other functions. I don't understand this comment in 4.3. Do you still believe it? Is it worth mentioning?