eclair

The development of high-quality software is a tough task: ECLAIR has been designed to assist development and quality assurance teams to realize that quality, as well as helping quality control teams assess its achievement.

What ECLAIR Is

ECLAIR is a powerful platform for the automatic analysis, verification, testing and transformation of C and C++ programs (with an ongoing extension to Java and a planned extension to other languages). [ECLAIR schematics]

ECLAIR is very flexible and highly configurable. It can support your software development workflow and environment, whatever they are. You can ask us to bend it to your precise needs or you can do that yourself.

ECLAIR is suitable for light verification tasks that can be run right on the developer's desktop, as well as for tough semantics-based analyses to be run overnight.

ECLAIR is fit for use in mission- and safety-critical software projects: it has been designed from the outset so as to exclude false negatives unless the user’s configuration explicitly asks for them.

ECLAIR is developed in a rigorous way and carefully checked also with extensive internal testsuites (counting tens of thousands of testcases) and industry-standard validation suites (such as ACE SuperTest).

ECLAIR is based on solid scientific research results and on the best practices of software development. Beware of the theory-practice false dichotomy: a truly reliable and practical system can only be based on rigorous theoretical investigation.

ECLAIR is developed by a passionate team of experts. Do not hesitate to let us have your feedback: you may be surprised to discover just how much your suggestions matter to us.

What ECLAIR Is Not

ECLAIR is not something that will tell you which software analysis, verification and testing activities are appropriate in your field. In particular, it cannot tell you which coding rules are suited to your project. However, the programming language experts at BUGSENG can provide significant help in this respect.

ECLAIR Features at a Glance

Supported Applications

Automatic Checking of Coding Standards

ECLAIR provides support for automatically checking conformance with respect to a number of widely used coding standards, among which:

• CERT C;
• EC--;
• MISRA C:1998;
• MISRA C:2004;
• The Power of Ten (C);
• NASA/JPL C;
• Netrino Embedded C;
• ESA/BSSC C/C++;
• CERT C++;
• MISRA C++:2008;
• JSF C++;
• High-Integrity C++;
• Delphi C;
• Industrial Strength C++;
• Nokia Qt (C++).

In addition to these, BUGSENG has developed checkers to verify conformance with respect to several other coding standards, including proprietary company standards and project-specific standards. Coding rules are enforced using very general and accurate checkers, which operate on the precise sequences of tokens and abstract syntax trees that are manipulated by the compiler.^{1This is in sharp contrast with checkers that are based on pattern matching and imprecise parsing. If, on the one hand, they can deal with programs that do not compile, on the other hand they are plagued by a high number of false positives and, most importantly, false negatives, something that makes them unsuitable to safety-critical and mission-critical contexts. Generally speaking, beware of tools based on obsolete technology: directives such as 90/385/EEC and 93/42/EEC in the medical sector assert that compliance can only be claimed if the generally acknowledged state-of-the-art is followed.} Coupled with the fact that ECLAIR always checks each rule in the appropriate context (at the token, declaration, translation unit, whole program or whole system levels), this makes sure that the checkers for decidable rules are exact (neither false positives nor false negatives). For undecidable rules, ECLAIR provides different checkers characterized by different solutions to the tradeoff among computational complexity, number of false positives and number of false negatives. In any case, when false negatives are possible, they are always clearly and unambiguously delimited.

ECLAIR can be configured to produce all sorts of violation reports:

• for immediate or later browsing using popular IDEs like Eclipse, Microsoft Visual Studio, IAR Embedded Workbench®, or any suitable editor (a very powerful, web-based browser is currently in beta-test);
• for the automatic insertion into issue-tracking systems or any other database;
• for the automatic production of compliance matrices required to meet industrial standards and guidelines such as IEC 61508, ISO 26262 (automotive), CENELEC EN 50128 (railway), DO-178B/C (aerospace), IEC 62304 and FDA norms (medical).

Semantic Analysis

We are equipping ECLAIR with powerful constraint propagation, symbolic model checking, and abstract interpretation engines. Their combined use allows the realization of different compromises between computational complexity and precision, so that each user can select an optimal cost-benefit tradeoff with respect to her objectives. On the developer's desktop, quick analyses are the most appropriate; but when the alternative is between, e.g., proving absence of run-time errors by hand or by machine, 12 hours of computation time is nothing: ECLAIR has been designed to support the entire spectrum between these two extremes.

Automatic Unit Test Case Generation

ECLAIR can automatically synthesize minimal sets of unit test inputs that reach a specified coverage criterion (or prove that such coverage cannot be reached due to infeasible conditions in the program). If a human or mechanized "oracle" is available to predict the expected output, then complete unit tests can be synthesized in a fraction of the time required for manual generation.

Semantic Matcher and Patcher

ECLAIR can perform very sophisticated program transformations by automatically finding program regions in the source identified by syntactic and semantics-based criteria, optionally replacing the matching program fragment with a parametrized substitution.

Other Applications

Simplifiers, obfuscators, translators, ... these are just a few examples of the plethora of applications that, because of ECLAIR’s highly modular design, can be developed relatively easily at the right level of abstraction. For instance, ECLAIR includes a C simplifier: it reads any valid C translation unit and (taking into account the implementation-defined aspect of the considered C implementation) it writes equivalent but much simplified C code (e.g., where side effects have been removed from expressions).

Proper Integration with the Toolchain

ECLAIR intercepts every invocation of the toolchain components (compilers, linker, assembler, archive manager) and it automatically extracts and interprets the options that the build system has passed to them. This allows for the seamless integration with any build system. Moreover, the user does not need to engage in error-prone activities such as:

• specifying which files compose the application and where the right header files are located;
• configuring the static analyzer so that the analysis parameters match the options given to the compilers (several options do affect the program semantics).

All this is automatic and supports build processes that involve the automatic generation of source files that depend on the configuration, without requiring the development and maintenance of a separated analysis procedure: with ECLAIR the existing build procedure can be used verbatim.

One of the key properties of ECLAIR is that it understands all the analysis-relevant options of the supported compilers. The language used to abstractly model such options is so powerful that adding support for a new compiler is no longer a problem.

Web-Based Configuration Interface

All the verification tasks supported by ECLAIR can be specified and refined incrementally by means of a very convenient web-based configuration interface. From any web browser this allows, for instance: finding coding rules using a powerful tag-based selection logic; activating and customizing coding rules, possibly restricting their use to only part of the project; selecting and customizing the kind of reports and compliance matrices to be generated; fine-tuning the semantic treatment of each elementary operation (particularly for undefined- and implementation-defined behaviors) in model-checking and automatic test data generation; choosing to run the verification task immediately or save the task for later.

Precise Parsing of Source Files

ECLAIR includes a state-of-the-art parser for C and C++ languages. In particular, for:

• the pre-standardization K&R C dialect;
• the standardized C languages (C90, C99 and C11);
• the standardized C++ languages (C++98, C++03 and C++11);
• the language extensions of the GNU C/C++ dialects (except for a few, deprecated ones);
• the language extensions of the Microsoft C/C++ dialects.

Work is in progress to support other extensions (e.g., OpenCL and CUDA) as well as the Java language.

The parser produces an accurate abstract syntax tree (AST) representing all of the information available in the analyzed code. Accuracy means, among other things, that:

• the AST represents not only the explicit, but also all of the implicit language constructs in the source code: implicit type conversions, compiler-generated functions (e.g., not explicitly defined constructors), instantiations of function/class templates, etc.;
• all language constructs are provided with precise location information, enabling the generation of reports pointing to the exact source of a violation.

Source location information is not only precise, but also thorough:

• complete information is available for the chain of file inclusions and, orthogonally, for the chain of macro expansions that brought a lexical token to become part of the analyzed code;
• the well-known difficulty of tracking problems in implicit template instantiations is solved presenting to the user complete yet easily readable information about the full instantiation chain.

Supported Platforms and Development Environments

ECLAIR is available on most modern flavors of Unix®, Linux, Mac OS X® and Windows®, including Cygwin and MinGW, and can be used with just about any development environment. Thanks to its ability to intercept the toolchain components, it supports all sorts of makefile-based, script-based or hybrid build systems. ECLAIR can leverage the availability of computing resources by supporting parallel and distributed program analyses. Most popular C/C++ compilers and cross compilers are supported, including Code Warrior™, GCC, Green Hills®, IAR, Intel®, Microsoft®, MPLAB®, Renesas Electronics, clang/LLVM.