Experience report: OCaml for an industrial-strength static analysis framework

ABSTRACT

This experience report describes the choice of OCaml as the implementation language for Frama-C, a framework for the static analysis of C programs. OCaml became the implementation language for Frama-C because it is expressive. Most of the reasons listed in the remaining of this article are secondary reasons, features which are not specific to OCaml (modularity, availability of a C parser, control over the use of resources...) but could have prevented the use of OCaml for this project if they had been missing.

REFERENCES

• 1: Patrick Baudin, Anne Pacalet, Jacques Raguideau, Dominique Schoen, and Nicky Williams. Caveat: a tool for software validation. In phDependable Systems and Networks, 2002, pages 537 , 2002.
• 2: Patrick Baudin, Jean-Christophe Filliâtre, Thierry Hubert, Claude Marché, Benjamin Monate, Yannick Moy, and Virgile Prevosto. phACSL: ANSI C Specification Language (preliminary design V1.4), preliminary edition, October 2008. URL http://frama-c.cea.fr/acsl.html.
• 3: Géraud Canet, Pascal Cuoq, and Benjamin Monate. A value analysis for C programs, 2009. To appear in the proceedings of SCAM2009.
• 4: Sylvain Conchon and Jean-Christophe Filliâtre. A persistent union-find data structure. In ML '07: Proceedings of the 2007 workshop on Workshop on ML, pages 37--46, New York, NY, USA, 2007. ACM. ISBN 978-1-59593-676-9. http://doi.acm.org/10.1145/1292535.1292541.
• 5: Sylvain Conchon, Jean--Christophe Filliâtre, and Julien Signoles. Designing a generic graph library using ML functors. In Marco T. Morazán, editor, Trends in Functional Programming, volume 8 of phTrends in Functional Programming, pages 124--140. Intellect, UK/The University of Chicago Press, USA, 2008. ISBN 978-1-84150-196-3.
• 6: Pascal Cuoq. Documentation of Frama-C's value analysis plug-in, 2008. URL http://frama-c.cea.fr/download/frama-c-manual-Lithium-en.pdf.
• 7: Pascal Cuoq and Damien Doligez. Hashconsing in an incrementally garbage-collected system: a story of weak pointers and hashconsing in OCaml 3.10.2. In ML '08: Proceedings of the 2008 ACM SIGPLAN workshop on ML, pages 13--22, New York, NY, USA, 2008. ACM. ISBN 978-1-60558-062-3.
• 8: David Delmas, Stéphane Duprat, Patrick Baudin, and Benjamin Monate. Proving temporal properties at code level for basic operators of control/command programs. In ph4th European Congress on Embedded Real Time Software, 2008.
• 9: Jean-Christophe Filliâtre and Sylvain Conchon. Type-safe modular hash-consing. In ML '06: Proceedings of the 2006 workshop on ML, pages 12--19, New York, NY, USA, 2006. ACM. ISBN 1-59593-483-9.
• 10: Xavier Leroy. A syntactic theory of type generativity and sharing. Journal of Functional Programming, 6: 1--32, 1996.
• 11: Yaron Minsky. Caml trading: Experiences in functional programming on Wall Street. In Wouter Swierstra, editor, The Monad. Reader, April 2007.
• 12: Benjamin Monate and Julien Signoles. Slicing for security of code. In Peter Lipp, Ahmad-Reza Sadeghi, and Klaus-Michael Koch, editors, phTRUST, volume 4968 of Lecture Notes in Computer Science, pages 133--142. Springer-Verlags, March 2008.
• 13: Ravi Nanavati. Experience report: a pure shirt fits. SIGPLAN Not., 43 (9): 347--352, 2008. ISSN 0362-1340.
• 14: George C. Necula, Scott Mcpeak, Shree P. Rahul, and Westley Weimer. CIL: Intermediate language and tools for analysis and transformation of C programs. In International Conference on Compiler Construction, pages 213--228, 2002.
• 15: Famantanantsoa Randimbivololona, Jean Souyris, Patrick Baudin, Anne Pacalet, Jacques Raguideau, and Dominique Schoen. Applying formal proof techniques to avionics software: A pragmatic approach. In FM '99: Proceedings of the Wold Congress on Formal Methods in the Development of Computing Systems-Volume II, pages 1798--1815, London, UK, 1999. Springer-Verlag. ISBN 3-540-66588-9.
• 16: Morten Rhiger. A foundation for embedded languages. ACM Transactions on Programming Languages and Systems (TOPLAS), 25 (3): 291--315, 2003. ISSN 0164-0925.
• 17: Julien Signoles. Plug-in development guide, 2008. URL http://frama-c.cea.fr/download/plug-in_development_guide.pdf.
• 18: Julien Signoles. Foncteurs impératifs et composés: la notion de projets dans Frama-C. In Actes des Journées Francophones des Langages Applicatifs, pages 37--54, January 2009. In French.

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.1 Applicative (Functional) Programming

General Terms:
Design, Languages, Verification

Keywords:
OCaml, plug-ins, software architecture, static analysis