ECLAIR

ECLAIR
DeveloperBUGSENG
Stable release
3.14.0 (2025) / May 12, 2025; 12 months ago (2025-05-12)[1]
Operating systemCross-platform
TypeStatic code analysis
LicenseProprietary
Websitebugseng.com/eclair-static-analysis-tool/

ECLAIR is a commercial static code analysis tool developed by BUGSENG for automatic analysis, verification, testing and transformation of C and C++ programs.

Capabilities

ECLAIR is a complete re-engineering of a series of prototypes[2] developed at the Applied Formal Methods Laboratory of the University of Parma. It uses formal methods-based static code analysis techniques such as abstract interpretation and model checking combined with constraint satisfaction techniques to detect or prove the absence of certain run time errors in source code, and provides support for program analysis and verification, program test generation and program transformation.

Concerning program analysis and verification, ECLAIR can statically detect or proof the absence of run-time anomalies as well as automatically check for conformance with respect to several coding standards, such as MISRA C, MISRA C++, CERT C Secure Coding Standard, CERT C++ Secure Coding Standard,[3] High-Integrity C++, NASA/JPL C, ESA/BSSC C/C++, JSF C++, EC--,[4] Netrino Embedded C,[5] The Power of Ten (C),[6] Industrial Strength C++.[7]

For program testing, ECLAIR can automatically synthesize sets of unit test inputs that reach a user-specified coverage criterion, warning the user when, due to infeasible conditions in the program, this coverage cannot be attained.

Regarding program transformation, ECLAIR can be used to perform complex program transformations: these are specified by syntactic and semantics-based criteria; the program regions in the source that match these criteria can be optionally replaced by a parametrized substitution.

See also

References

  1. ^ "News BUGSENG". bugseng.com. Retrieved 2021-04-04.
  2. ^ R. Bagnara; P. M. Hill; E. Zaffanella (2007). "A Prolog-based Environment for Reasoning about Programming Languages". arXiv:0711.0345 [cs.PL].
  3. ^ Seacord, Robert C. (2013). Secure Coding in C and C++. SEI Series in Software Engineering (2nd ed.). Addison-Wesley Professional. ISBN 978-0-321-82213-0.
  4. ^ Hatton, L. (2005). "EC—a measurement based safer subset of ISO C suitable for embedded system development". Information and Software Technology. 47 (3): 181–695. CiteSeerX 10.1.1.101.7828. doi:10.1016/j.infsof.2004.08.001.
  5. ^ Barr, Michael (2008). Embedded C Coding Standard. Barr Group. ISBN 978-1442164826.
  6. ^ Gerald, J. (2006). "The Power of 10: Rules for Developing Safety-Critical Code". Computer. 39 (6): 95–97. Bibcode:2006Compr..39f..95H. doi:10.1109/MC.2006.212. S2CID 7334261.
  7. ^ Henricson, Mats; Nyquist, Erik (1997). Industrial Strength C++. Prentice-Hall PTR. ISBN 978-0131209657.

Content Disclaimer

Informasi ini disarikan dari Wikipedia dan disajikan kembali untuk tujuan edukasi. Konten tersedia di bawah lisensi CC BY-SA 3.0. Kami tidak bertanggung jawab atas ketidakakuratan data yang bersumber dari kontribusi publik tersebut.

  1. The information displayed on this website is sourced in part or in whole from Wikipedia and has been adapted for the purpose of restating it. We strive to provide accurate and relevant information, however:
  2. There is no guarantee of absolute accuracy. Wikipedia is an open, collaborative project that can be edited by anyone, so information is subject to change.
  3. It is not intended to constitute professional advice. The content displayed is for informational and educational purposes only. For important decisions (e.g., medical, legal, or financial), please consult a professional.
  4. Content copyright. Wikipedia is licensed under the Creative Commons Attribution-ShareAlike License (CC BY-SA). This means that content may be reused with appropriate attribution and shared under a similar license.
  5. Responsible use. Any risk arising from the use of information from this website is entirely the responsibility of the user.