From 745808dea711cca2c056e5de6715df5e4627f315 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 2 Sep 2019 09:45:51 +0200
Subject: [PATCH] [Variadic] Fixes a bug related to pointer to function with
 ghost parameters

---
 .../tests/declared/function-ptr-with-ghost.c  |  8 ++++
 .../oracle/function-ptr-with-ghost.res.oracle | 42 +++++++++++++++++++
 src/plugins/variadic/translate.ml             |  3 +-
 3 files changed, 52 insertions(+), 1 deletion(-)
 create mode 100644 src/plugins/variadic/tests/declared/function-ptr-with-ghost.c
 create mode 100644 src/plugins/variadic/tests/declared/oracle/function-ptr-with-ghost.res.oracle

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 00000000000..0ab1f1a1c0c
--- /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 00000000000..d23f5b52381
--- /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 0dbf07862c4..6e7e7c72125 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
-- 
GitLab