Use the nuw attribute of GEPs to prove that pointers do not alias, in cases matching the following: + + + | BaseOffset | +<nuw> Indices | ---------------->|-------------------->| |-->V2Size | |-------> V1Size LHS RHS If the difference between pointers is Offset +<nuw> Indices then we know that the addition does not wrap the pointer index type (add nuw) and the constant Offset is a lower bound on the distance between the pointers. We can then prove NoAlias via Offset u>= V2Size.
79 KiB
79 KiB