Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

The Art of Developing Frama-C Plug-ins

  • Chapter
  • First Online:
Guide to Software Verification with Frama-C

Part of the book series: Computer Science Foundations and Applied Logic ((CSFAL))

  • 211 Accesses

Abstract

One of the key features of Frama-C is its extensibility. More precisely, the platform is based on a kernel, which provides the core services and datastructures that are needed for analyzing C programs, including in particular parsing C and ACSL code. Analyses themselves are then implemented by plug-ins, that use the kernel’s API to, among other things, access the code under analysis, perform some code transformation, add ACSL annotations, and validate (or invalidate) other ACSL annotations. Furthermore, plug-ins can also export their own API to be used by other plug-ins. In this chapter, we will give an overview of Frama-C ’s general architecture and describe the main functionalities of the kernel, using as example a small plug-in that we build step by step during the course of the chapter.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 54.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Hardcover Book
USD 69.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    https://ocaml.org.

  2. 2.

    https://v2.ocaml.org/releases/4.14/htmlman/index.html.

  3. 3.

    https://ocaml.org/docs.

  4. 4.

    https://www.electronjs.org/.

  5. 5.

    https://react.dev/.

  6. 6.

    Actually, it would also be possible to provide a specific domain for Eva to propagate typestate information together with the rest of Eva ’s abstract state. Building Eva domains is presented in Chap. 3.

  7. 7.

    https://dune.build/.

  8. 8.

    This will be used for packaging the plug-in, as shown in Sect. 7.8.2.

  9. 9.

    In addition to .core, some complex plug-ins also define sub-packages with names such as frama-c-plugin.subpkg, but this is outside the scope of this chapter.

  10. 10.

    We do not provide any interface file options.mli: adding it is left as an exercise for the developer.

  11. 11.

    https://github.com/ocaml/odoc.

  12. 12.

    https://ocaml.github.io/odoc/odoc_for_authors.html#doc-pages.

  13. 13.

    File src/libraries/utils/pretty_utils.mli.

  14. 14.

    Full details available in the Plug-in Development Guide [14], Sect. Logging Services.

  15. 15.

    Modulo the preprocessing phase, since Frama-C parses the source code after the preprocessor has run.

  16. 16.

    Since there are few functions in the API, we don’t really need to use a more efficient datastructure. For larger mappings, Sect. 7.5.1 will show how to define maps and hash tables.

  17. 17.

    Our plug-in doesn’t attempt to handle arrays of file or struct with file fields. See Exercise 6 in Sect. 7.6.3.

  18. 18.

    Note that Db.Postdominators’s values are references to functions, hence they must be dereferenced before being called.

  19. 19.

    Frama-C ’s module Integer is an extension of module Z from the Zarith library provided at https://github.com/ocaml/Zarith/.

  20. 20.

    In a future version of Frama-C, datatypes will be automatically generated in most cases through ppx extensions.

  21. 21.

    This mechanism allows Frama-C to customize how to unserialize OCaml values, which is particularly useful for hashconsed values [4, 5]. There is no need to customize the serialization process, which is always the default OCaml one.

  22. 22.

    Except the few parameters explicitly prevented from being registered through a call to Parameter_customize.do_not_projectify.

  23. 23.

    Only the first function is memoized since it is often more useful in practice.

  24. 24.

    As explained in Chap. 2, in the normalized AST of Frama-C, each function has exactly one return statement.

  25. 25.

    https://dune.readthedocs.io/en/stable/tests.html#cram-tests.

  26. 26.

    https://opam.ocaml.org/.

  27. 27.

    https://nixos.org/.

  28. 28.

    The universe dependency indicates to always rerun this rule when requested.

  29. 29.

    This might be handled automatically by Dune in future releases.

  30. 30.

    Currently, uploading the source code archive of the plugin is only possible for plug-ins hosted on Github.

  31. 31.

    Even if this chapter assumes knowledge of OCaml for understanding it, several developers with no expertise in functional languages in general and in OCaml in particular have already developed Frama-C plug-ins. Basically, they have just practiced a bit by reading and applying some OCaml tutorials before developing their own plug-ins.

References

  1. Allen FE (1970) Control flow analysis. In: Proceedings of a symposium on compiler optimization. Association for computing machinery, New York, NY, USA. https://doi.org/10.1145/800028.808479

  2. Appel AW (2004) Modern compiler implementation in ML. Cambridge University Press

    Google Scholar 

  3. Cousot P (2021) Principles of abstract interpretation. MIT Press

    Google Scholar 

  4. Cuoq P, Doligez D (2008) Hashconsing in an incrementally garbage-collected system: a story of weak pointers and Hashconsing in Ocaml 3.10.2. In: Workshop on ML. https://doi.org/10.1145/1411304.1411308

  5. Cuoq P, Doligez D, Signoles J (2011) Lightweight typed customizable unmarshaling. In: Workshop on ML

    Google Scholar 

  6. Cuoq P, Signoles J, Baudin P, Bonichon R, Canet G, Correnson L, Monate B, Prevosto V, Puccetti A (2009) Experience report: OCaml for an industrial-strength static analysis framework. In: International conference of functional programming (ICFP)

    Google Scholar 

  7. Gamma E, Helm R, Johnson R, Vlissides J (1994) Design patterns: elements of reusable object-oriented software. Addison-Wesley

    Google Scholar 

  8. Hickey J, Madhavapeddy A, Minsky Y (2021) Real world OCaml, 2nd ed. O’Reilly (2021). https://dev.realworldocaml.org/

  9. Kildall GA (1973) A unified approach to global program optimization. In: Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on principles of programming languages, POPL ’73, pp 194–206. Association for Computing Machinery. https://doi.org/10.1145/512927.512945

  10. Michie D (1968) Memo functions and machine learning. Nature

    Google Scholar 

  11. Nielson F, Nielson HR, Hankin C (2015) Principles of program analysis. Springer

    Google Scholar 

  12. Rival X, Yi K (2020) Introduction to static analysis: an abstract interpretation perspective. MIT Press

    Google Scholar 

  13. Signoles J (2009) Foncteurs impératifs et composés: la notion de projet dans Frama-C. In: Journées Francophones des Langages Applicatifs (JFLA). In French

    Google Scholar 

  14. Signoles J, Antignac T, Correnson L, Lemerre M, Prevosto V, Plug-in development guide. http://frama-c.com/download/frama-c-plugin-development-guide.pdf

  15. Strom RE, Yemini S (1986) Typestate: a programming language concept for enhancing software reliability. IEEE Trans Softw Eng 12(1)

    Google Scholar 

  16. Whitington J (2013) OCaml from the very beginning. Coherent Press

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Université Paris-Saclay, CEA, List, Palaiseau, France

    François Bobot, André Maroneze, Virgile Prevosto & Julien Signoles

Authors
  1. François Bobot
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. André Maroneze
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Virgile Prevosto
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Julien Signoles
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to François Bobot .

Editor information

Editors and Affiliations

  1. Thales Research & Technology, Palaiseau, France

    Nikolai Kosmatov

  2. Software Safety and Security Laboratory, Université Paris-Saclay, CEA, List, Gif-sur-Yvette, France

    Virgile Prevosto

  3. Software Safety and Security Laboratory, Université Paris-Saclay, CEA, List, Gif-sur-Yvette, France

    Julien Signoles

Rights and permissions

Reprints and permissions

Copyright information

© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Bobot, F., Maroneze, A., Prevosto, V., Signoles, J. (2024). The Art of Developing Frama-C Plug-ins. In: Kosmatov, N., Prevosto, V., Signoles, J. (eds) Guide to Software Verification with Frama-C. Computer Science Foundations and Applied Logic. Springer, Cham. https://doi.org/10.1007/978-3-031-55608-1_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-55608-1_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-55607-4

  • Online ISBN: 978-3-031-55608-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation