This patch lets GCC to determine which registers to save when we
switch to/from a VCPU in the case of AMD i386

* Original code saves following registers:

    ebx, ecx, edx, esi, edi, ebp

* Patched code:

  - informs GCC that we modify following registers
    using the clobber description:

    ebx, ecx, edx, esi, edi

  - rbp is saved (pop/push) because GCC seems to ignore its use in the clobber
    description.
Signed-off-by: NLaurent Vivier <Laurent.Vivier@bull.net>
Signed-off-by: NAvi Kivity <avi@qumranet.com>