Skip to content

Draft: Remove requirement that task should not contain include statements

Hernan Ponce de Leonrequested to merge
preprocessing into main

In the community meeting from 2024-11-05, we voted to remove the requirement that verification tasks should not contain #include statements starting in SVCOMP 2026. While this might require verification tools to perform the preprocessing on their own, participants have now a full year to work on this.

This does not mean we are immediately getting rid of preprocessed files, but it should enable a transition period in which any of *.c and *.i files might be used in the task definition. In the meeting today we could not identify any technical reason why this would be a problem.

Since I expect this MR to generate some debate, pinging some of the people that contributed to the discussion today, and others that I expect to have an opinion.

@strejcek @sim642 @schuessf @vesal.vojdani @rmonat @dbeyer @PhilippWendler

Merge request reports