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...
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.
addinG a spark test file with nnested procedures.
Fixed the dirty compiler for better portability.
Configuration made better + comments + small refactoring.
Nested procedure seem to work (not the out parameter yet).

+ The main procedure is found when compiling the global declaration.
+ cleaning some parts.
Copy_out for procedures implemented.
disserting in idee.txt + proc2 compleified.
Fix in compilation of spark nested procedure.
Generated assembly works!

+ Fixed wrong duplication of params in local vars
+ Test file
+ Fixed cminor generation from spark.
Added a Makefile for testing spark compilation + somes tests.
Tests are working modulo 2 workarounds of sireum.

Namely sed'ing the .cm files to put function names.
and setting the procedure levels by hand in .v files.
Tests work with still one manua phase.
Fixed testing compile chain temporarily waiting for sireum.
Sireum has been adapted byt Zhi, example work once de-workaround.

Still: recursive procedures are not correctly generated by sireum.
Added a test file for the demo at Adacore (2014, nov 5th).
Registering the names for variables + removing patches to Compcert.
Starting the proof of transl_expr_ok. Variables are ok.
Adding a _CoqProject file to Compcert.