Modelling of alignement constraints is too strict

[vbgl]

The current memory model used for defining semantics Jasmin and assembly languages mandates that any access of size N is done at an address multiple of N.

This is a good property to ensure: the compiler only emits aligned accesses (supposedly good for performances, sometimes required by the ISA).

But it is a too strong property to require, in particular from user code. It also seems to prevent loading arguments from the stack.

[vbgl]

Done in #748