You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
This repository has been archived by the owner on Oct 3, 2021. It is now read-only.
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.
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.
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.
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.
The text was updated successfully, but these errors were encountered:
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
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.make preprocessed
in the directory where I changed some.c
files and I would not need to worry about doing this manually..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..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.The text was updated successfully, but these errors were encountered: