Use gettimeofday() instead of obsolete ftime().
(Patch by Daniel Dickman.)
Record public global definitions via field "prog_public" in AST.program.
For the moment, this field is ignored.
Add Genv.public_symbol operation.
Restrict pointer event values to public global names.
Update proofs accordingly.  PowerPC and ARM need updating.
Verification of the Unusedglob pass (removal of unreferenced static global definitions).  Assorted changes to ia32/Op.v.  PowerPC and ARM need updating.
Update PowerPC port.
Update the ARM port.
Merge pull request #2 from AbsInt/public-globals

Public globals
Use Bitstring.is_zeroes_bitstring from bitstring 2.0.4.
The original code is less efficient and not tail recursive.
Wrong handling of block-local function declarations (in Elab.ml).
Changed the comparison of jumptables.
Removed unused variable and changed the search for the installation directory. Use Sys.executable_name instead of Sys.argv.(0).
Removed more unused variables.
Preserve single quotes (e.g. in CPREPRO) when generating compcert.ini
Prevent constant propagation on Oindirectsymbol addresses.
(Otherwise they are turned into Oaddrsymbol or global addressing modes,
causing linking issues on MacOS X.)
Update the IA32/MacOS X port.
- Prefix symbols with _
- Print indirect symbol definitions
- Suppress __asm() macros in system header files
Stdlib path is ignored when the configuration has_runtime_lib is set to false.
Prototype the pointer so that the program has well defined semantics and passes the reference interpreter.
Merge branch 'master' of https://github.com/AbsInt/CompCert
Use cp instead of symbolic links for executables.
Now that we search for compcert.ini from Sys.executable, symbolic links cause compcert.ini not to be found.
Clean up support for common symbols.  Uninitialized "const" symbols can be common.