Add global variables to AutomataSystem

[ghost]

As far as I can understand, static global variables, which is not taken an address of (or an address of any supertype) could be used as a single variable, and no memory model magic is needed. (Which is a pain at the moment when preparing gazer-theta for XCFA formalism)
Note that recursive functions would need a non-local variable.

int global_variable; // not static -> other code might use the variable through extern int global_variable;

// if the code contains &global, then variable x cannot be inlined
struct X {
  int x;
} global_struct;

// if the code contains &array[3] or array+i, etc., then "array[5]" should not be inlined(?)
int array[10];

I'm thinking of writing it as an LLVM pass + a modification to AutomataSystem, but I don't know:
1) ... whether this property (the variable is not taken an address of) is enough. Am I missing something?
e.g. SROA can actually help, probably only primitive types will be interesting for me
2) ... how to prevent memory modelling pass to "kick in" for these vars (annotate the memory object?), which is probably better than undoing the MemSSA. Is there, by chance, something already doing this?
3) ... how hard it is for AutomataSystem to support globals (a variable used in more than one function). Are there anything to keep in mind? (I'm thinking that adding a variable store directly to the AutomataSystem should be enough)

Can someone help me with answering these questions?