Abstract: Heap-manipulating programs usually operate memory cells directly through shared and mutable data-struc- tures,which makes their memory safety more complex and harder to guarantee. A field-sensitive k-limit abstract memory model was proposed in this paper to support dynamic adjustment of the precision and efficiency of the analysis .We presented its framework, property and operations. And then,four kinds of memory-related errors were identified in the operational semantics of the abstract memory model according to the definition of memory safety. In the end, we pro- posed the dataflow iteration algorithm for detecting the memory safety of C programs.

Key words: Heap-manipulating programs, Memory safety, k-limit abstract memory model, Dynamic adjustment