Skip to content

Use unpreprocessed files in task definitions

This is part 2 of two closely related issues, the first one (#1123) building the base for implementing this one.

We could try to allow for unpreprocessed program files to be used in task definition files and expect the tools to preprocess the files according to the headers that we would specify in the SV-COMP rules. The necessary prequisites for this would be established by #1123. The overhead in execution time arising from the preprocessing should be negligible.

The yml files would of course also have to be adapted to refer to the .c files instead of the .i files. They would also be somewhat underspecified since the headers are only fixed by our convention. We could however also add the headers to the task definition,the format even allows wildcards such that we can add a while folder with headers with just one include/*.h

The tools might then naturally be extended with a --includedir option where the user can specify the headers to be used for preprocessing. This is a cool feature in itself because currently the verifiers that can already preprocessed C files probably just take the system default headers, which might actually not be the ones that will be used for the actual compilation of the program (I am thinking about embedded systems as an example here). This preprocessor step could of course also just be done by a small tool that is provided by us and wrapped around the actual tool execution.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information