diff --git a/src/plugins/variadic/tests/declared/function-ptr-with-ghost.c b/src/plugins/variadic/tests/declared/function-ptr-with-ghost.c
new file mode 100644
index 0000000000000000000000000000000000000000..0ab1f1a1c0c7e5597794b56a0192ee6cb5cf9206
--- /dev/null
+++ b/src/plugins/variadic/tests/declared/function-ptr-with-ghost.c
@@ -0,0 +1,8 @@
+void function(void (*p) (int, ...) /*@ ghost (int v) */, int x){
+  (*p) (x, 1, 2, 3) /*@ ghost (4) */;
+}
+void va_f(int, ...) /*@ ghost(int x) */ ;
+
+int main(void){
+  function(va_f, 3);
+}
\ No newline at end of file
diff --git a/src/plugins/variadic/tests/declared/oracle/function-ptr-with-ghost.res.oracle b/src/plugins/variadic/tests/declared/oracle/function-ptr-with-ghost.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..d23f5b523810e4f0743338a780bb6d9041a04d43
--- /dev/null
+++ b/src/plugins/variadic/tests/declared/oracle/function-ptr-with-ghost.res.oracle
@@ -0,0 +1,42 @@
+[variadic] tests/declared/function-ptr-with-ghost.c:4: 
+  Declaration of variadic function va_f.
+[variadic] tests/declared/function-ptr-with-ghost.c:2: 
+  Generic translation of call to variadic function.
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[kernel:annot:missing-spec] tests/declared/function-ptr-with-ghost.c:2: Warning: 
+  Neither code nor specification for function va_f, generating default assigns from the prototype
+[eva] using specification for function va_f
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function function:
+  
+[eva:final-states] Values at end of function main:
+  __retres ∈ {0}
+/* Generated by Frama-C */
+void function(void (*p)(int , void * const *__va_params)/*@ ghost (int v) */,
+              int x)
+{
+  {
+    int __va_arg0 = 1;
+    int __va_arg1 = 2;
+    int __va_arg2 = 3;
+    void *__va_args[3] = {& __va_arg0, & __va_arg1, & __va_arg2};
+    (*p)(x,(void * const *)(__va_args))/*@ ghost (4) */;
+  }
+  return;
+}
+
+/*@ assigns \nothing; */
+void va_f(int, void * const *__va_params)/*@ ghost (int x) */;
+
+int main(void)
+{
+  int __retres;
+  function(& va_f,3);
+  __retres = 0;
+  return __retres;
+}
+
+
diff --git a/src/plugins/variadic/translate.ml b/src/plugins/variadic/translate.ml
index 0dbf07862c4da167cad784fc1e547b6b06f098f9..6e7e7c7212514305affbbdb957b0f0facbb6de33 100644
--- a/src/plugins/variadic/translate.ml
+++ b/src/plugins/variadic/translate.ml
@@ -173,7 +173,8 @@ let translate_variadics (file : file) =
       | Call(lv, callee, args, loc) ->
         let is_variadic =
           try
-            let last = Extends.List.last (Typ.params (Cil.typeOf callee)) in
+            let args, _ = Typ.ghost_partitioned_params (Cil.typeOf callee) in
+            let last = Extends.List.last args in
             last = Generic.vpar
           with Extends.List.EmptyList -> false
         in