C global variables "temporarily unsupported"

[andrewj-brown]

I'm interested in verifying C programs for information flow security, and it's rather difficult to provide useful examples without the use of global variables.

From what I can glean so far, there appears to be an error in constructing the AST, where it assumes "declarators" always have parameters (or their inner types have parameters, for arrays and pointers).

How difficult of a fix is this likely to be? I may be able to attempt it, but it looks like it might involve going through many levels of the parser to convince it that parameter-less expressions are ok in a top-level context.

[pieter-bos]

I've resolved this on the dev branch. You should be able to treat them as any other heap location now, see e.g. here: https://github.com/utwente-fmt/vercors/blob/dev/examples/concepts/clang/c-example-use.c.

[andrewj-brown]

Wow, that was quick! That's fantastic, thanks heaps.