Abstract
Runtime assertion checking provides a powerful, highly automatizable technique to detect violations of specified program properties. This paper provides a lesson on runtime assertion checking with Frama-C, a publicly available toolset for analysis of C programs. We illustrate how a C program can be specified in executable specification language e-acsl and how this specification can be automatically translated into instrumented C code suitable for monitoring and runtime verification of specified properties. We show how various errors can be automatically detected on the instrumented code, including C runtime errors, failures in postconditions, assertions, preconditions of called functions, and memory leaks. Benefits of combining runtime assertion checking with other Frama-C analyzers are illustrated as well.
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
Clarke, L.A., Rosenblum, D.S.: A historical perspective on runtime assertion checking in software development. ACM SIGSOFT Software Engineering Notes 31(3), 25–37 (2006)
Correnson, L., Cuoq, P., Kirchner, F., Prevosto, V., Puccetti, A., Signoles, J., Yakobowski, B.: Frama-C User Manual (April 2013), http://frama-c.com
Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C, a program analysis perspective. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 233–247. Springer, Heidelberg (2012)
Baudin, P., Filliâtre, J.C., Hubert, T., Marché, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI/ISO C Specification Language, v1.6. (April 2013), http://frama-c.com/acsl.html
Signoles, J.: E-ACSL: Executable ANSI/ISO C Specification Language (May 2013), http://frama-c.com/download/e-acsl/e-acsl.pdf
Delahaye, M., Kosmatov, N., Signoles, J.: Common specification language for static and dynamic analysis of C programs. In: The 28th Annual ACM Symposium on Applied Computing (SAC 2013), pp. 1230–1235. ACM (2013)
Signoles, J.: E-ACSL User Manual (May 2013), http://frama-c.com/download/e-acsl/
Meyer, B.: Object-Oriented Software Construction. Prentice-Hall, Inc. (1988)
Leavens, G.T., Cheon, Y., Clifton, C., Ruby, C., Cok, D.R.: How the design of JML accommodates both runtime assertion checking and formal verification. Sci. Comput. Program. 55(1-3), 185–208 (2005)
Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005)
AdaCore and Altran UK Ltd: SPARK 2014 Reference Manual (2013), http://docs.adacore.com/spark2014-docs/html/lrm/
Kosmatov, N., Prevosto, V., Signoles, J.: A lesson on proof of programs with Frama-C. Invited tutorial paper. In: Veanes, M., Viganò, L. (eds.) TAP 2013. LNCS, vol. 7942, pp. 168–177. Springer, Heidelberg (2013)
Kosmatov, N., Petiot, G., Signoles, J.: Optimized memory monitoring for runtime assertion checking of C programs. In: The 4th International Conference on Runtime Verification (RV 2013). LNCS. Springer (2013) (to appear)
Botella, B., Delahaye, M., Hong-Tuan-Ha, S., Kosmatov, N., Mouy, P., Roger, M., Williams, N.: Automating structural testing of C programs: Experience with PathCrawler. In: The 4th Int. Workshop on Automation of Software Test (AST 2009), pp. 70–78. IEEE Computer Society (2009)
Cousot, P.R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238–252 (1977)
Dijkstra, E.W.: A constructive approach to program correctness. BIT Numerical Mathematics (1968)
Conchon, S., et al.: The Alt-Ergo Automated Theorem Prover, http://alt-ergo.lri.fr/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kosmatov, N., Signoles, J. (2013). A Lesson on Runtime Assertion Checking with Frama-C. In: Legay, A., Bensalem, S. (eds) Runtime Verification. RV 2013. Lecture Notes in Computer Science, vol 8174. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40787-1_29
Download citation
DOI: https://doi.org/10.1007/978-3-642-40787-1_29
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-40786-4
Online ISBN: 978-3-642-40787-1
eBook Packages: Computer ScienceComputer Science (R0)