[variadic] Fixes ghost formals decl

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
 

src/plugins/variadic/tests/defined/maintain-formals-order.i

+/*@ 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) */;
+}

src/plugins/variadic/tests/defined/oracle/maintain-formals-order.res.oracle

+[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;
+}
+
+