Unlike other high level programming languages, the C programming language assumes a rather low level memory model and provides extensive kinds of memory operations, such as multi-level pointers, arbitrary pointer arithmetic, built-in array and struct data types.
Pointers in C can point to arbitrary locations of the memory, and can be cast freely between different types. All these make it difficult to simulate the C semantics accurately.
This paper describes a memory modeling method for static analysis of C programs. It is particularly suitable for precise path-sensitive analyses, e.g., symbolic execution.
It can handle almost all kinds of C expressions, including arbitrary levels of pointer dereferences, pointer arithmetic, composite array and struct data types, arbitrary type casts, dynamic memory allocation, etc.
It maps aliased value expressions to the identical object without extra alias analysis. The model has been implemented in the Clang static analyzer and enhanced the analyzer a lot by enabling it to have precise value tracking ability.
It enables the symbolic execution to identify and track each memory object precisely. We give algorithms that enable the mapping from C l-value expressions to memory objects during the analysis. Thus no separate alias analysis is required.
To read this external content in full download the paper from the author archives.