From 6f2efbe1cd93617f9dec519ef7ec1e0b820d67a6 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Sat, 22 Jan 2022 18:49:45 +0100
Subject: [PATCH] [Variadic] Add a test about the conversion of va_arg results

---
 .../defined/oracle/va_arg_cast.res.oracle     | 52 +++++++++++++++++++
 .../variadic/tests/defined/va_arg_cast.c      | 18 +++++++
 2 files changed, 70 insertions(+)
 create mode 100644 src/plugins/variadic/tests/defined/oracle/va_arg_cast.res.oracle
 create mode 100644 src/plugins/variadic/tests/defined/va_arg_cast.c

diff --git a/src/plugins/variadic/tests/defined/oracle/va_arg_cast.res.oracle b/src/plugins/variadic/tests/defined/oracle/va_arg_cast.res.oracle
new file mode 100644
index 00000000000..7d4f6bbe42c
--- /dev/null
+++ b/src/plugins/variadic/tests/defined/oracle/va_arg_cast.res.oracle
@@ -0,0 +1,52 @@
+[kernel:parser:decimal-float] va_arg_cast.c:17: Warning: 
+  Floating-point constant 7.1 is not represented exactly. Will use 0x1.c666666666666p2.
+  (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
+[variadic] va_arg_cast.c:10: Declaration of variadic function c.
+[variadic] va_arg_cast.c:17: 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 b:
+  a ∈ {4619679907765970542}
+  ap ∈ {{ &__va_args[2] }}
+[eva:final-states] Values at end of function c:
+  a ∈ {4619679907765970542}
+  ap ∈ {{ &__va_args[0] }}
+[eva:final-states] Values at end of function main:
+  a ∈ {4619679907765970542}
+/* Generated by Frama-C */
+#include "stdarg.h"
+long a;
+void b(va_list ap)
+{
+  long tmp;
+  a = (long)*((double *)*ap);
+  ap ++;
+  tmp = *((long *)*ap);
+  ap ++;
+  a += tmp;
+  return;
+}
+
+void c(int d, void * const *__va_params)
+{
+  va_list ap;
+  ap = __va_params;
+  b(ap);
+  return;
+}
+
+void main(void)
+{
+  {
+    double __va_arg0 = 8.1;
+    double __va_arg1 = 7.1;
+    void *__va_args[2] = {& __va_arg0, & __va_arg1};
+    c(0,(void * const *)(__va_args));
+  }
+  return;
+}
+
+
diff --git a/src/plugins/variadic/tests/defined/va_arg_cast.c b/src/plugins/variadic/tests/defined/va_arg_cast.c
new file mode 100644
index 00000000000..0f643ab6224
--- /dev/null
+++ b/src/plugins/variadic/tests/defined/va_arg_cast.c
@@ -0,0 +1,18 @@
+#include <stdarg.h>
+
+long a;
+
+void b(va_list ap) {
+  a = va_arg(ap, double);
+  a += va_arg(ap, long);
+}
+
+void c(int d, ...) {
+  va_list ap;
+  va_start(ap, d);
+  b(ap);
+}
+
+void main() {
+    c(0, 8.1, 7.1);
+}
-- 
GitLab