--- /dev/null
+--- xen-4.1.2/xen/arch/x86/i8259.c.orig 2011-10-20 18:05:48.000000000 +0100
++++ xen-4.1.2/xen/arch/x86/i8259.c 2012-01-15 00:37:08.583827754 +0000
+@@ -62,7 +62,7 @@
+ IRQ(x,8), IRQ(x,9), IRQ(x,a), IRQ(x,b), \
+ IRQ(x,c), IRQ(x,d), IRQ(x,e), IRQ(x,f)
+
+- static void (*interrupt[])(void) = {
++ static void (asmlinkage *interrupt[])(void) = {
+ IRQLIST_16(0x0), IRQLIST_16(0x1), IRQLIST_16(0x2), IRQLIST_16(0x3),
+ IRQLIST_16(0x4), IRQLIST_16(0x5), IRQLIST_16(0x6), IRQLIST_16(0x7),
+ IRQLIST_16(0x8), IRQLIST_16(0x9), IRQLIST_16(0xa), IRQLIST_16(0xb),
+--- xen-4.1.2/xen/include/asm-x86/hvm/svm/intr.h.orig 2011-10-20 18:05:50.000000000 +0100
++++ xen-4.1.2/xen/include/asm-x86/hvm/svm/intr.h 2012-01-15 16:38:13.199784658 +0000
+@@ -21,6 +21,6 @@
+ #ifndef __ASM_X86_HVM_SVM_INTR_H__
+ #define __ASM_X86_HVM_SVM_INTR_H__
+
+-void svm_intr_assist(void);
++asmlinkage void svm_intr_assist(void);
+
+ #endif /* __ASM_X86_HVM_SVM_INTR_H__ */
+--- xen-4.1.2/xen/include/asm-x86/hvm/vmx/vmx.h.orig 2011-10-20 18:05:50.000000000 +0100
++++ xen-4.1.2/xen/include/asm-x86/hvm/vmx/vmx.h 2012-01-15 17:06:07.495853077 +0000
+@@ -63,7 +63,7 @@
+
+ void vmx_asm_vmexit_handler(struct cpu_user_regs);
+ void vmx_asm_do_vmentry(void);
+-void vmx_intr_assist(void);
++asmlinkage void vmx_intr_assist(void);
+ void vmx_do_resume(struct vcpu *);
+ void vmx_vlapic_msr_changed(struct vcpu *v);
+ void vmx_realmode(struct cpu_user_regs *regs);