diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 99910c959b5045e6c547ec2e215a6ca8cd235ccd..eed9f317cc26cf824e5a21ff1d85c63cfd1a9748 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -6911,7 +6911,7 @@ module Switch_cases =
 let () = dependency_on_ast Switch_cases.self
 let separate_switch_succs = Switch_cases.memo separate_switch_succs
 
-class dropAttributes ?select () = object
+class dropAttributes ?select () = object(self)
   inherit genericCilVisitor (Visitor_behavior.copy (Project.current ()))
   method! vattr a =
     match select with
@@ -6924,8 +6924,9 @@ class dropAttributes ?select () = object
     | TNamed (internal_ty, attrs) ->
       let tty = typeAddAttributes attrs internal_ty.ttype in
       (* keep the original type whenever possible *)
-      ChangeDoChildrenPost
-        (tty, fun x -> if x == internal_ty.ttype then ty else x)
+      ChangeToPost
+        (visitCilType (self:>cilVisitor) tty,
+         fun x -> if x == internal_ty.ttype then ty else x)
     | TVoid _ | TInt _ | TFloat _ | TPtr _ | TArray _ | TFun _
     | TComp _ | TEnum _ | TBuiltin_va_list _ -> DoChildren
 end
diff --git a/src/plugins/variadic/tests/defined/oracle/simple.res.oracle b/src/plugins/variadic/tests/defined/oracle/simple.0.res.oracle
similarity index 88%
rename from src/plugins/variadic/tests/defined/oracle/simple.res.oracle
rename to src/plugins/variadic/tests/defined/oracle/simple.0.res.oracle
index 66ca05b979890b76bcd32c42a58475e1d5c7a2d1..d682b185f8e6766bf5acd7d25d211ac7cc35ba8d 100644
--- a/src/plugins/variadic/tests/defined/oracle/simple.res.oracle
+++ b/src/plugins/variadic/tests/defined/oracle/simple.0.res.oracle
@@ -1,5 +1,5 @@
-[variadic] simple.c:4: Declaration of variadic function sum.
-[variadic] simple.c:19: Generic translation of call to variadic function.
+[variadic] simple.c:9: Declaration of variadic function sum.
+[variadic] simple.c:24: Generic translation of call to variadic function.
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
diff --git a/src/plugins/variadic/tests/defined/oracle/simple.1.res.oracle b/src/plugins/variadic/tests/defined/oracle/simple.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..7b5221cf83de9df7862c7d97e175b5b68ddb6eba
--- /dev/null
+++ b/src/plugins/variadic/tests/defined/oracle/simple.1.res.oracle
@@ -0,0 +1,52 @@
+[variadic] simple.c:9: Declaration of variadic function sum.
+[variadic] simple.c:24: 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 sum:
+  ret ∈ {42}
+  i ∈ {5}
+  list ∈ {{ &__va_args[5] }}
+[eva:final-states] Values at end of function main:
+  
+/* Generated by Frama-C */
+typedef void * const *__gnuc_va_list;
+typedef __gnuc_va_list va_list;
+/*@ requires n ≥ 0; */
+int sum(int n, void * const *__va_params)
+{
+  va_list list;
+  int ret = 0;
+  int i = 0;
+  list = __va_params;
+  while (i < n) {
+    {
+      int tmp;
+      tmp = *((int *)*list);
+      list ++;
+      ret += tmp;
+    }
+    i ++;
+  }
+  return ret;
+}
+
+int main(void)
+{
+  int tmp;
+  {
+    int __va_arg0 = 6;
+    int __va_arg1 = 9;
+    int __va_arg2 = 14;
+    int __va_arg3 = 12;
+    int __va_arg4 = 1;
+    void *__va_args[5] =
+      {& __va_arg0, & __va_arg1, & __va_arg2, & __va_arg3, & __va_arg4};
+    tmp = sum(5,(void * const *)(__va_args));
+  }
+  return tmp;
+}
+
+
diff --git a/src/plugins/variadic/tests/defined/simple.c b/src/plugins/variadic/tests/defined/simple.c
index 132f956fcb98f2b1bbbccd6aa1e1a06c1994d390..b2346a3f09cadb78412a84f82bd1deca74232c59 100644
--- a/src/plugins/variadic/tests/defined/simple.c
+++ b/src/plugins/variadic/tests/defined/simple.c
@@ -1,3 +1,8 @@
+/* run.config
+STDOPT:
+STDOPT: #"-no-frama-c-stdlib -no-pp-annot"
+*/
+
 #include <stdarg.h>
 
 /*@ requires n>= 0; */