A points-to analysis computes a sound abstraction of heap memory conventionally using a name-based abstraction that summarizes runtime memory by grouping locations using the names of allocation sites: All concrete heap locations allocated by the same statement are grouped together. The locations in the same group are treated alike i.e., a pointer to any one location of the group is assumed to point to every location in the group leading to an over-approximation of points-to relations.

We propose an access-based abstraction that partitions each name-based group of locations into equivalence classes at every program point using an additional criterion of the sets of access paths (chains of pointer indirections) reaching the locations in the memory. The intuition is that the locations that are both allocated and accessed alike should be grouped into the same equivalence class. Since the access paths in the memory could reach different locations at different program points, our groupings change flow sensitively unlike the name-based groupings. This creates a more precise view of the memory. Theoretically, it is strictly more precise than the name-based abstraction except in some trivial cases; practically it is far more precise.

Our empirical measurements show the benefits of our tool Access-Based Heap Analyzer (ABHA) on SPEC CPU 2006 and heap manipulating SV-COMP benchmarks. ABHA scales to 20 kLoC and can improve the precision even up to 99% (in terms of the number of aliases). Additionally, ABHA allows any user-defined summarization of an access path to be plugged in; we have implemented and evaluated four summarization techniques. ABHA can also act as a front-end to TVLA, a parametrized shape analyzer, in order to automate its parametrization by generating predicates that capture the program behaviour more accurately.