This work presents a sound backward analysis for sufficient pre-conditions inference in C programs, by abstract interpretation.
It builds upon previous works done for a purely numeric subset of C, and extends them to support the C memory model.
Pointer dereferences are handled with the cell abstraction and dynamic memory allocations with the recency abstraction.
A direct usage of the abstract operators proposed in these previous works in an under-approximation framework is not possible as either internally they rely on over-approximated operators (e.g., cell removal) or an extension to this framework is not straightforward (e.g., under-approximating join).
In this work we propose new operators that are under-approximating, and on top of this we design a backward semantics.
The analysis is implemented in the MOPSA analyzer and its performance is assessed in detection of sufficient pre-conditions for runtime errors in 13,261 C tasks from NIST Juliet test suite.
