sosy-lab/sv-benchmarks

Do not track preprocessed files in this repository

MartinSpiessl opened this issue · 3 comments

This is part 1 of two closely related issues, the second one (#1124) building upon this one.

It has become more and more labor-intensive over the past years to maintain both the .c files and their preprocessed .i versions.

From a versioning point of view, the .i files actually do not need to be tracked as they can be automatically generated. Since this depends on the header files, those would need to be specified/versioned in order to ensure that the .i files can be reproduced byte by byte.

If we specified the header files here, we could even demand that tools support the unpreprocessed regular .c files, cf. issue #1124. To that end, we could even provide a self-contained preprocessing module that participants can use in their tool to generate the .i files on the fly. The preprocessing should always be fast compared to the actual verification, so the overhead that comes from this is actually negligible.

  1. As a first step, we could add targets to the Makefile that also do the preprocessing. This would already help for the PRs in this repository since I could simply run make preprocessed in the directory where I changed some .c files and I would not need to worry about doing this manually.
  2. Once all .i files can reliably be preprocessed on the fly via the make target, we can try to do this while only using a set of self-contained header files that are located in this repository.
  3. Then once this works, we have everything we need to get rid of the .i files (at least those that have a corresponding .c file). If someone still wants to have them on disk, they can generate them using the make target.

This is basically a duplicate of #122.

Thanks for the hint. But I guess after 5 years it makes sense to reevaluate some things. Also point 1. and 2. are actually useful regardless of whether we actually get rid of the .i files

#123 is also related.