From 2043362ef9f53234d9e23e0c61a89b969d97f853 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 22 Mar 2022 14:19:05 +0100
Subject: [PATCH] [kernel] ensure we correctly unroll typedefs in
 typeDeepDropAllAttributes

turns out that Change**DoChildren**Post does not visit the **head** node.
---
 src/kernel_services/ast_queries/cil.ml        |  7 +--
 ...{simple.res.oracle => simple.0.res.oracle} |  4 +-
 .../tests/defined/oracle/simple.1.res.oracle  | 52 +++++++++++++++++++
 src/plugins/variadic/tests/defined/simple.c   |  5 ++
 4 files changed, 63 insertions(+), 5 deletions(-)
 rename src/plugins/variadic/tests/defined/oracle/{simple.res.oracle => simple.0.res.oracle} (88%)
 create mode 100644 src/plugins/variadic/tests/defined/oracle/simple.1.res.oracle

diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 99910c959b5..eed9f317cc2 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 66ca05b9798..d682b185f8e 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 00000000000..7b5221cf83d
--- /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 132f956fcb9..b2346a3f09c 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; */
-- 
GitLab