diff --git a/src/plugins/variadic/generic.ml b/src/plugins/variadic/generic.ml
index d7298e5b82029e29df4500a8fe4aeba123e0cd67..586d6041d62af0615c852996638b45362bfb81e5 100644
--- a/src/plugins/variadic/generic.ml
+++ b/src/plugins/variadic/generic.ml
@@ -58,12 +58,13 @@ let translate_type = function
 
 let add_vpar vi =
   let formals = Cil.getFormalsDecl vi in
+  let n_formals, g_formals = List.partition (fun v -> not v.vghost) formals in
   (* Add the vpar formal once *)
   if not (List.exists (fun vi -> vi.vname = vpar_name) formals) then
     begin
       (* Register the new formal *)
       let new_formal = Cil.makeFormalsVarDecl vpar in
-      let new_formals = formals @ [new_formal] in
+      let new_formals = n_formals @ [new_formal] @ g_formals in
       Cil.unsafeSetFormalsDecl vi new_formals
     end
 
diff --git a/src/plugins/variadic/tests/defined/maintain-formals-order.i b/src/plugins/variadic/tests/defined/maintain-formals-order.i
new file mode 100644
index 0000000000000000000000000000000000000000..4c525164291ee7619d63f6e5165cfc88458ca923
--- /dev/null
+++ b/src/plugins/variadic/tests/defined/maintain-formals-order.i
@@ -0,0 +1,16 @@
+/*@ requires c == 0 && x == 1 ; */
+void f(int x,...) /*@ ghost(int c) */ {
+  /*@ ghost int g = c; */
+}
+
+/*@ requires c == 0 && x == 1 && y == 2; */
+void g(int x, int y,...) /*@ ghost(int c) */ {
+  /*@ ghost int g = c; */
+}
+
+void main(void){
+  f(1) /*@ ghost(0) */;
+  f(1, 2, 3) /*@ ghost(0) */;
+
+  g(1, 2, 3, 4) /*@ ghost(0) */;
+}
diff --git a/src/plugins/variadic/tests/defined/oracle/maintain-formals-order.res.oracle b/src/plugins/variadic/tests/defined/oracle/maintain-formals-order.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..814fcfccf9b5141dbf6b66536f66b7bafc37085d
--- /dev/null
+++ b/src/plugins/variadic/tests/defined/oracle/maintain-formals-order.res.oracle
@@ -0,0 +1,58 @@
+[variadic] tests/defined/maintain-formals-order.i:2: 
+  Declaration of variadic function f.
+[variadic] tests/defined/maintain-formals-order.i:7: 
+  Declaration of variadic function g.
+[variadic] tests/defined/maintain-formals-order.i:12: 
+  Generic translation of call to variadic function.
+[variadic] tests/defined/maintain-formals-order.i:13: 
+  Generic translation of call to variadic function.
+[variadic] tests/defined/maintain-formals-order.i:15: 
+  Generic translation of call to variadic function.
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function f:
+  g_0 ∈ {0}
+[eva:final-states] Values at end of function g:
+  g_0 ∈ {0}
+[eva:final-states] Values at end of function main:
+  
+/* Generated by Frama-C */
+/*@ requires c ≡ 0 ∧ x ≡ 1; */
+void f(int x, void * const *__va_params) /*@ ghost (int c) */
+{
+  /*@ ghost int g_0 = c; */
+  return;
+}
+
+/*@ requires c ≡ 0 ∧ x ≡ 1 ∧ y ≡ 2; */
+void g(int x, int y, void * const *__va_params) /*@ ghost (int c) */
+{
+  /*@ ghost int g_0 = c; */
+  return;
+}
+
+void main(void)
+{
+  {
+    void *__va_args[1] = {(void *)0};
+    f(1,(void * const *)(__va_args)) /*@ ghost (0) */;
+  }
+  {
+    int __va_arg0 = 2;
+    int __va_arg1 = 3;
+    void *__va_args_5[2] = {& __va_arg0, & __va_arg1};
+    f(1,(void * const *)(__va_args_5)) /*@ ghost (0) */;
+  }
+  {
+    int __va_arg0_7 = 3;
+    int __va_arg1_9 = 4;
+    void *__va_args_11[2] = {& __va_arg0_7, & __va_arg1_9};
+    g(1,2,(void * const *)(__va_args_11)) /*@ ghost (0) */;
+  }
+  return;
+}
+
+