Detecting unnecessary reads/modifies entries

[parno]

Would it be reasonable for Vale to detect when you've included an entry in your reads or modifies clause that isn't actually needed? For example, if I include rax in my modifies list, but nothing in the procedure actually modifies it, it would be helpful to at least produce a warning, since this often leads to subtle proof failures in later code. E.g., code that expects (correctly) that the value in rax will be preserved across this procedure call, but the fact that it's included in the modifies clause leads to a proof failure. A slightly more subtle case is when you include something in the modifies clause that really only needs to be in the reads clause.