Idea: Program analyses/annotation for not verifying 'dead code'

[sakehl]

So with C/CUDA/OpenCL files we can and should include headers. These headers are automatically inserted in the file send to VerCors, due to the preprocessor.

But if functionality of a header is never used, it is still verified by VerCors.

There are several things to consider here.

• We could make all functions in headers abstract. This helps, but can cause unsoundness.

  • The unsoundness can be counteracted to also have a version of the header with a concrete implementation, from which we automatically generate the abstract headers. Or something similar.

• Even if all functions are abstract, we still do the 'pre-condition is not false' check, thus still overhead.

• We could also add an annotation, which marks a function to be not checked. Something like /*@ unchecked @*/ or /*@ header @*/. Then if such a function is included, we always make it abstract/do not check the precondition. Or we could do a dead-code analyses, which removes any such function if it is never called.

I don't think it matters to much at the moment, but some header files can get quite big, thus could lead to slower verification if we keep adding new features.

It also pollutes the generated .vpr files with backend-file-base which is annoying but meh.