Strong update — the assignments overwrite the contents of the target property, is essential for precise static analysis of memory operations. Classically, the strong update is safe if such assignment will definitely occur and that it assigns to a unique location.

We find that this classic safety condition of strong update can be weakened if we semantically restrict our analysis to a limited scope of program identifiers, which we will call “targets” in this work. This finding allows us to systematically discover more strong update cases by picking up the appropriate targets.

Our experimental results confirm this finding. In our earlier work, we have developed a static analysis that is able to infer numerical properties for large-scale Java programs. The analysis introduces symbolic variables upon which the “weak update” has to be applied in the classical sense so that the underlined locations reflected by these symbolic variables potentially retain its old values. By selecting as the targets the program identifiers that are used literally in program, we are able to apply “strong update” in many cases where such abstraction is unsafe in the classic sense.