To be able to model global variables that use features of C not supported by litmus, or to be able to hide global variables from litmus, we could do with support for a second form of global variables. These would differ from the existing variables in several ways:
No representation in the test itself and, therefore, no set-up by the harness;
The above implies the variable persists between iterations;
Form an actual global variable initialiser, and can have qualifiers added.
As far as I can tell, this would involve doing the following:
[ ] Figure out some way of extending the litmus representation to understand nonstandard extension blocks;
[ ] Make an extension block for C that contains non-litmus variables (and, eventually, non-litmus functions, etc etc);
[ ] Make the delitmusifier able to handle the extension block by either emitting it directly or complaining about its existence (according to the delitmus style);
[ ] Figure out some way of making these variables useful without the guarantee that litmus will refresh the value every pass (perhaps we'll statically initialise it to a value, but then also forbid any further non-idempotent stores);
[ ] Teach the fuzzer etc. to use the non-litmus variables where possible, to avoid polluting Litmus's global variable pool.
To be able to model global variables that use features of C not supported by litmus, or to be able to hide global variables from litmus, we could do with support for a second form of global variables. These would differ from the existing variables in several ways:
As far as I can tell, this would involve doing the following: