It should be, actually, as long as you give it all the source code or give it object files with the summary data in them.
The summary mod/ref info should be enough to get it right, because it should say the function does not modify the argument, and that should get propagated through.
The tricky case is where it sometimes modifies the argument - the summary data is not flow sensitive, IIRC
Flow sensitive algorithms are still really expensive worst case (N^3 minimum, sometimes exponential), but could be made practical here using BDD's. Most compilers still do not use BDD's to represent this sort of large binary decision data, even though they are very good at it. It's an area where research always felt more advanced than production (IE even if you don't go whole-hog on datalog, the data structures are still very useful for this sort of otherwise-memory/time intensive data)
