What does this experimental data mean?

This is experimental data from compiling and running our C memory object model tests on various C implementations and analysis tools.

The tests

Our test cases are typically written to illustrate a particular semantic question as concisely as possible. Some are "natural" examples, of desirable C code that one might find in the wild, but many are intentionally pathological or are corner cases, to explore just where the defined/undefined-behaviour boundary is; we are not suggesting that all these should be supported.

Making the tests concise to illustrate semantic questions also means that most are not written to trigger interesting compiler behaviour, which might only occur in a larger context that permits some analysis or optimisation pass to take effect. Moreover, following the spirit of C, conventional implementations cannot and do not report all instances of undefined behaviour. Hence, only in some cases is there anything to be learned from the experimental compiler behaviour. For any executable semantics or analysis tool, on the other hand, all the tests should have instructive outcomes.

Some tests rely on address coincidences for the interesting execution; for these we sometimes include multiple variants, tuned to the allocation behaviour in the implementations we consider. Where this has not been done, some of the experimental data is not meaningful.

The platforms

The tests have been run with a range of tools:

The Charon test harness

The tests are run using a test harness, charon, that generates individual test instances from JSON files describing the tests and tools; charon logs all the compile and execution output (together with the test itself and information about the host) to another JSON file for analysis. The tests and harness can be packaged up in a single tarball that can be run easily. charon also supports cross-compilation, to let the tests be compiled on a normal host and executed on other hardware.