SpringerLink
Log in

Tools for Program Understanding

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

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

  • 23 Accesses

Abstract

Frama-C can operate as an exploration framework: several plug-ins and scripts have been created to enable tool-assisted code exploration and understanding. Unassisted reviews of C code require deep expertise and knowledge of many of C ’s pitfalls; Frama-C should help overcome many of its quirks, to help ensure that “all bugs are shallow”. Whether you want some simple metrics and an overview; or you need to quickly evaluate code written by others; or you seek deep understanding about the origin of a complex bug, several Frama-C plug-ins are available to help you. This chapter presents these plug-ins and provides pointers for further details.

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
EUR 32.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
EUR 29.95
Price includes VAT (Thailand)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
EUR 53.49
Price includes VAT (Thailand)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Hardcover Book
EUR 64.99
Price excludes VAT (Thailand)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free ship** worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    This pivot table component is currently based on an external library, react-pivottable.

  2. 2.

    See Chap. 2 for information about machdeps.

  3. 3.

    Standards-compliant code would simply use uint64_t from <inttypes.h>, but in practice much code is not standards-compliant.

  4. 4.

    Note that, currently, build_commands.json files are not automatically produced by any tool; the Frama-C team intends to release such a tool in the nearby future to help automate this step.

  5. 5.

    https://clang.llvm.org/docs/JSONCompilationDatabase.html.

  6. 6.

    https://github.com/rizsotto/Bear.

  7. 7.

    https://www.brendangregg.com/flamegraphs.html.

  8. 8.

    https://embed.cs.utah.edu/creduce/.

References

  1. Bonichon R, Yakobowski B, Frama-C’s metrics plug-in. https://www.frama-c.com/download/frama-c-metrics-manual.pdf

  2. Correnson L, Cuoq P, Kirchner F, Maroneze A, Prevosto V, Puccetti A, Signoles J, Yakobowski B, Frama-C user manual. https://www.frama-c.com/download/frama-c-user-manual.pdf

  3. Wilkes M (1985) Memoirs of a computer pioneer. Massachusetts Institute of Technology, USA

    Google Scholar 

Download references

Author information

Authors and Affiliations

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

    André Maroneze & Valentin Perrelle

Authors
  1. André Maroneze
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Valentin Perrelle
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to André Maroneze .

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

Maroneze, A., Perrelle, V. (2024). Tools for Program Understanding. 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_8

Download citation

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

  • 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