Test the extraction to EasyCrypt

[eponier]

We were reported a few bugs (https://github.com/jasmin-lang/jasmin/issues/128, https://github.com/jasmin-lang/jasmin/issues/130, https://github.com/jasmin-lang/jasmin/issues/135) of the extraction to EasyCrypt recently, it would be good to have tests for it, because it seems we have none for the moment. The tests would be complementary to having libjade in the CI (which would be good too).

[tfaoliveira]

After reading this issue I ran some experiments on compiler/examples/. You can find some files attached to this message. I extracted each function from each file under this directory (at the top of each file you can see the command that I used to achieve this):

• compiler_examples_jobs.log - this file contains the list of commands that I used to get the results of the following file; maybe it can be used as a basis to test the extraction to EC using code under compiler/examples;
• compiler_examples_easycrypt.log - this file contains the output of running the previous commands; some issues are detected;
• compiler_examples_easycrypt_critical_or_error.log - selection of lines containing 'critical' or 'error'

For this test, the missing operators are:

named `adc_64
named `Array16
named `Array8
named `MOV_64
named `sbb_64

And there are also some "Assertion failed":

"src/toEC.ml", line 480
"src/toEC.ml", line 721