From f7b4e88fa8ac2c093c0a75e77c1f0fd6956d92f6 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 11 Dec 2020 15:01:15 +0100
Subject: [PATCH] [variadic] Fixes ghost formals decl

---
 src/plugins/variadic/generic.ml               |  3 +-
 .../tests/defined/maintain-formals-order.i    | 16 +++++
 .../oracle/maintain-formals-order.res.oracle  | 58 +++++++++++++++++++
 3 files changed, 76 insertions(+), 1 deletion(-)
 create mode 100644 src/plugins/variadic/tests/defined/maintain-formals-order.i
 create mode 100644 src/plugins/variadic/tests/defined/oracle/maintain-formals-order.res.oracle

diff --git a/src/plugins/variadic/generic.ml b/src/plugins/variadic/generic.ml
index d7298e5b820..586d6041d62 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 00000000000..4c525164291
--- /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 00000000000..814fcfccf9b
--- /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;
+}
+
+
-- 
GitLab