Modified toCL to be able to run reduce4 mulx example and added the reduce4 mulx example

[JoaoDiogoDuarte]

Depends on #944 and #945.

This merge request adds:

• reduce4.jazz example with abstract predicates and asserts/assumes that will result in a valid and correct cryptoline file

And adds the following translations:

• ADOX
• ADCX
• MULX

and changes the IMULr translation to include an assert.

[lyonel2017]

@JoaoDiogoDuarte can you address my previous remarks.

[JoaoDiogoDuarte]

@JoaoDiogoDuarte can you address my previous remarks.

I'd be happy to, but I don't see any on any remarks in any of the pull requests concerning cryptoline. Do you mind writing them down please? Apologies if you already said them in one of our meetings.

[lyonel2017]

I think this is wrong. The adcs instruction in Cryptoline cannot be used for both ADCX and ADOX in both signed and unsigned mode. I would say adcs can be used for ADCX in unsigned mode, and for ADOX in signed mode. But require to be checked.