CEA List and Solid Sands entered into a partner agreement to make SuperTest available to the Frama-C team. Frama-C is a platform for source-code analysis of C software. The Frama-C analyzers assist with various source-code-related activities, including verifications and semantic analysis to find undefined behavior. Naturally, we asked ourselves: what happens if we use SuperTest and Frama-C to verify each other?
Frama-C is not a compiler, but it has many similarities: it parses programs, types them, and produces an AST. More importantly, it can analyze tests semantically.
SuperTest is not a normal program, but a collection of, sometimes contrived, tests that touch every aspect of C. It will stress any tool that processes C. Its positive tests should be strictly conforming to the C standard.
Given enough C programs, cracks will appear
Solid Sands has analyzed many implementations of C and C analysis tools. We have never seen any implementation that is free of error. That is not to say that there are no good implementations. It is just that in the corners of the language there are things that you can easily trip over. Another difficult issue to get right is the precision of diagnostics. Hence, some errors in Frama-C were to be expected.
Vice versa, from Frama-C’s previous experience with test suites and benchmarks, at least some semantic bugs in SuperTest were to be expected: given a sufficiently large set of C programs, and given the large amount of subtle semantic aspects in the language, it is statistically unlikely to obtain such a suite completely free of undefined behaviors, be them portability issues, non-deterministic cases, or simply bugs.
Eva to the rescue
The Eva plug-in of Frama-C is particularly efficient for this kind of scenario: mostly automatic execution, no (or few) specifications needed and great precision due to small test sizes.
After an initial setup to configure parsing and adjust a few stubs (e.g. so that Eva will consider the most general case), it is often easy to run Frama-C and obtain precise results in a few minutes. In SuperTest, interpreting the results is made easier by the fact that test cases are named and structured according to the corresponding C standard features they test.
Given enough C programs, Frama-C will fail to parse some
Before starting the test campaign, the Frama-C team expected Frama-C to not completely succeed with it. Frama-C’s parser is not 100% compatible with ISO C: it tends to be too lenient. The main reasons being that:
- Frama-C does not compile the code, so the user will have to write syntactically valid C code in the end; historically, Frama-C delegates some checks to the compiler;
- Frama-C focuses on semantic analyses, leaving the thorny bits of syntactic issues to other, better-suited tools. For instance, Frama-C does not even have its own preprocessor.
Nowadays, the Frama-C team strives to make the platform as syntactically compliant as possible, but there are still a few remaining spots requiring some polish. SuperTest certainly helps with that.
Results: unsurprising, but interesting nonetheless
Unsurprisingly, we found both kinds of issues: some semantic issues in SuperTest, and some syntactic shortcomings in the case of Frama-C. Actually, we found more of the latter than the former.
Fortunately, we found no major problems. The issues found in SuperTest are of little relevance for critical and embedded systems – for instance, issues related to wide characters. We believe two reasons are that (1) many tools and frameworks decide not to support these functions, since they are rarely used in the domain of embedded systems; and (2) the issues were related to portability, and thus undetectable in some architectural configurations.
Final score: win-win
Overall, this interchange between CEA List and Solid Sands has proven beneficial to both: setting up a recurrent run of Frama-C on SuperTest prevents regressions and also benefits from evolutions to Frama-C itself; on the other hand, Frama-C can improve its syntactic support thanks to SuperTest.
André Maroneze, Researcher/ Engineer at CEA List
Vladislav Yaglamunov, Software Engineer & Marcel Beemster, CTO at Solid Sands