Parser produces unhelpful error message near .gh include

[JoergPfaehler]

If I have some non-ghost statements (directly?) before an include of a .gh file I always get a parser error (without any useful hint as to what is going on).

example.c:

typedef int int_t;
//@ #include "example.gh"

and an empty example.gh.

[btj]

The only use case for both real and ghost includes that we have ever considered is header files, where the includes are at the top of the file without other preprocessor directives or program declarations intervening.

If your intention is that example.gh will use int_t, then that will not work, because in the interest of sound linking, each header file is typechecked in isolation, so int_t is not in scope inside example.gh. The solution is to declare int_t in some other header file and have example.gh include that header file.

Except that ghost headers can include only ghost headers and ghost headers cannot declare typedefs. I guess one way for us to fix this would be to allow real includes inside ghost headers but check at the point where the ghost header is included that the real headers included by the ghost header were already included earlier and therefore the real includes inside the ghost header are no-ops (assuming all headers have proper header guards). I opened #47 to track this.

The workaround is to turn the ghost header into a real header.

If, however, you intend example.gh to be parametric in int_t, and to be usable with different values for int_t in different .c files: this, too, is not yet supported, and for this a different, somewhat more involved, fix would be needed. The problem is if example.gh declares (lemma) function prototypes. If a .c file includes example.gh and implements such a prototype, say for lemma function foo, then this is recorded in the .vfmanifest file as implements example.gh#foo. If some other .c file includes example.gh and calls the lemma, this is recorded in its .vfmanifest file as requires example.gh#foo. VeriFast's link check checks that each module's requirements are satisfied by preceding modules' implementations. But if the meaning of the contract of foo is different in both cases, then this check is not sound. So, to support parameterized headers, we need to explicitly include the "argument values" for the "header parameters" in the .vfmanifest file. For example, one could get a line implements example.gh(int_t=int)#foo in the first module's .vfmanifest file, and a line requires example.gh(int_t=long long)#foo in the second module's.

[JoergPfaehler]

Thanks for the detailed explanation, Bart! It is actually quite easy for me to fix (there is no parametricity or anything; I just put that into the example for the bug report). So I think I would be perfectly happy with a better error message if that is easily possible.

[btj]

Oh, OK. I'm reopening the issue to track that.