You’re right, the second function is argmemonly. I jumped ahead to trying to create a sound rule, but it’s not an exact one. The actual underlying issue I was getting at is this: You need to ensure that other functions which are called transitively also only access memory passed as argument to the function you want to mark as argmemonly. For example, if foo calls bar and bar accesses global memory, foo can’t be argmemonly.
The reason for that is: Generally, a property like “the function does not do X” means that “during the execution of the function, X does not happen”. Put differently, it doesn’t matter whether X happens literally in the function itself or is delegated to another function — the effect from the caller’s point of view is the same. That’s because the caller’s point of view is what matters if you want to optimize a call to the function that is claimed to not do X, and also because function calls may be inlined.
Well, after you’ve optimized the former to the latter, they are equivalent. The distinction only exists if you analyze the source program without any simplification. One optimization allowing further optimizations that were hampered by the code that was optimized away is a common theme.