Exploring C Semantics and Pointer Provenance: Supplementary Material

• Exploring C Semantics and Pointer Provenance. Kayvan Memarian, Victor B. F. Gomes, Brooks Davis, Stephen Kell, Robert N. M. Watson, Peter Sewell. In Proc. 46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019).

It comprises:

1. a link to the Cerberus web interface

2. basic provenance test data, per test. The experimental data from running each of our basic provenance tests within Cerberus and on various other systems (GCC, Clang, ICC, sanitisers, CompCert, RV-Match). This data is also linked to from within the Cerberus web interface.

3. basic provenance test data, summary spreadsheet and in .xlsx

4. basic provenance test suite: the test sources for the above

5. the test log files for the above

6. the GCC torture tests used for validation, taken from https://github.com/gcc-mirror/gcc/tree/master/gcc/testsuite/gcc.c-torture/execute Here are the manual changes made in these tests, and the README summarises the test results.

7. the ITC-Toyota tests used for validation, taken from https://github.com/Toyota-ITC-SSD/Software-Analysis-Benchmark. The results are summarised here in pdf and ods.

8. the KCC example tests used for validation, taken from https://github.com/kframework/c-semantics/tree/master/examples/c.
   The README summarises the test results.

9. the Csmith tests used for validation.

10. the CHERI BSD change annotations, in the repository https://github.com/CTSRD-CHERI/cheribsd, can be found at https://github.com/CTSRD-CHERI/cheribsd/commit/ccc5c30683c1cefaf1d1f6f45c3d171db54c6c46 and https://github.com/CTSRD-CHERI/cheribsd/commit/c24a8afa2b25d59edb7548fe55ff89581947cc17