Removed duplicated open.
Deactivated the warning for deprecated features for compilation of cchecklink since it breaks the build with newer ocaml versions.
Tune behavior wrt warnings:
- cchecklink was compiled with -warn-error, which is bad for production code
- silence warning 3 (deprecated functions)
- silence warning 20 (unused function argument) for Coq-extracted files.
cchecklink: added option "-files-from" to read .sdump file names
from a file or from standard input.
build_from_parsed: simplified code + correctness proof.
Revised parsing of command-line arguments (in preparation for adding more).
Honor "ccomp -E foo.h" for GCC compatibility.
Accept .o.ext files as object files for GCC compatibility.
Fixed and improved handling of Cminor source files.
Add flags to control individual optimization passes + flag -O0 for turning them off.
Analysis of jump tables was using the wrong size.
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
Adding things to compcert to accept the spark frontend.

For the moment this is done in an absolutely hackish way: via
extraction + output_value + input_value of the sireum output...
spark related gitignore.
A first compilation process from spark to assembly.

Very ugly hack for the moment:
foo.adb --sireum bakar--> foo.v
foo.v  --patch + extraction--> foo.ml
foo.ml --patch marshal + compilation + execution --> foo.mlo (marshalled ml values)
foo.mlo (marshalled ml values) --spark2Cminor+compcert--> foo.s (+foo.cm).
Adding a cleaning script to spark test directory.
adjusting gitignore.