Increase Traceability and Reduce Maintenance Effort for Verification Tasks

[dbeyer]

• How to generate the .i files automatically from the .c files?
• How to remember architecture dependencies?
• How to better reflect what the intentions of a verification tasks are and were it comes from?

[tautschnig]

At a much larger scale, Linux distributions have solved these problems properly, so it's not that rocket science would be required. I had myself made attempts in the benchmarking toolkit (http://www.cprover.org/software/benchmarks/), and also benchexec has a notion of configuration files to permit reproducible results. I am happy to discuss this here in detail, or else leave it for a future in-person meeting with a wider group.

Best,
Michael

[delcypher]

How to generate the .i files automatically from the .c files?
How to remember architecture dependencies?

The build system already knows what the target is (x86_64-unknown-linux-gnu or i386-unknown-linux-gnu) so that most logical thing to do is to teach the build system to build the *.i files from the *.c files. The changes needed to the build system to do this are pretty trivial and actually vastly simplifies the current implementation.

A reproducible environment is also required if you want consistent *.i files between Linux distributions using different versions of glibc. One option is just to provide a canonical environment (i.e. a VM or a docker image) that the build should be performed in, my preference would be a docker image as they are much more light weight.

An alternative option to a VM or docker image is to actually provide the headers you want to use in the repository (i.e. in a include/ directory), pass -nostdinc to the compiler and pass -I include/ to the compiler so that we control what files are included. I'm not a huge fan of this idea as it means we have to maintain our own C library header files.

If we have a consistent way to generate *.i files then should NOT be stored in the repository as this is a waste of space. We would provide instructions on how to obtain the *.i files and/or provide nightly builds and also a final (for the competition) snapshot build.

[tautschnig]

So #121 is all about this, and there are discussions on the mailing list. I think we have a vast collection of technical solutions proposed. @PhilippWendler @dbeyer It's now a question of what can be implemented within the constraints of the competition run-time system, or for what there is willingness to implement it.