Abstract
Automatic bug finding with static analysis requires precise tracking of different memory object values. 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 lvalue 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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Cadar, C., Twohey, P., Ganesh, V., Engler, D.: EXE: A system for automatically generating inputs of death using symbolic execution. Technical report, Computer System Laboratory, Stanford University (2006)
Clang static analyzer, http://clang-analyzer.llvm.org/
Godefroid, P., Klarlund, N., Sen, K.: DART: Directed automated random testing. In: Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, pp. 213–223 (2005)
Hampapuram, H., Yang, Y., Das, M.: Symbolic path simulation in path-sensitive dataflow analysis. In: Proceedings of the 6th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, pp. 52–58 (2005)
WG14 ISO/IEC 9899:201x, editor. Programming Languages - C. ISO (1999), http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1336.pdf
Kremenek, T.: Finding bugs with the clang static analyzer, http://llvm.org/devmtg/2008-08/Kremenek_StaticAnalyzer.pdf
The LLVM compiler infrastructure, http://llvm.org/
Nielson, H.R., Nielson, F.: Semantics with applications: a formal introduction. John Wiley & Sons Inc., Chichester (1992)
Xie, Y., Aiken, A.: Saturn: A scalable framework for error detection using Boolean satisfiability. ACM Transactions on Programming Languages and Systems 29(3) (2007)
Xu, Z., Zhang, J.: A test data generation tool for unit testing of C programs. In: Proceedings of the International Conference on Quality Software, pp. 107–116 (2006)
Zhang, J.: Symbolic execution of program paths involving pointers and structure variables. In: Proceedings of the Fourth International Conference on Quality Software, pp. 87–92 (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Xu, Z., Kremenek, T., Zhang, J. (2010). A Memory Model for Static Analysis of C Programs. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification, and Validation. ISoLA 2010. Lecture Notes in Computer Science, vol 6415. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16558-0_44
Download citation
DOI: https://doi.org/10.1007/978-3-642-16558-0_44
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-16557-3
Online ISBN: 978-3-642-16558-0
eBook Packages: Computer ScienceComputer Science (R0)