C is widely used in safety-critical systems, therefore it is important to have static analysis tools that can automatically identify program properties and thus help in the search for bugs. I will present C-2PO, a weakly-relational pointer analysis that can infer relationships between pairs of pointer terms in C programs, including pointer arithmetic and dereferencing. It is based on the 2-Pointer Logic introduced by Seidl et al. and is extended with the concept of block disequalities that express the confinement of pointers to single memory objects in C. Abstract operations are introduced that allow the implementation of C-2PO in an abstract interpretation framework, including the operations meet, join, widening, and narrowing, as well as the abstract effects for assignments. C-2PO is implemented in the Goblint static analyzer. Lastly, I will discuss experimental results of C-2PO to evaluate its precision and efficiency.
