Public globals

As recently discussed on the compcert-users mailing list, this branch marks global definitions as either public (visible from the outside) or static (private to the compilation unit).  Then, pointer values exchanged with the outside world (e.g. results of volatile read operations) are restricted to public global names.  
This makes it possible to prove the correctness of compilation passes that add or remove static global definitions.  As an application, this branch proves the correctness of the Unusedglob pass (removal of unreferenced static definitions), which was not verified before.